Paper doi abstract bibtex

In this paper we develop a functional programming language for quantum computers by extending the simply-typed lambda calculus with quantum types and operations. The design of this language adheres to the ‘quantum data, classical control’ paradigm, following the first author's work on quantum flow-charts. We define a call-by-value operational semantics, and give a type system using affine intuitionistic linear logic. The main results of this paper are the safety properties of the language and the development of a type inference algorithm.

@article{selinger_lambda_2006, title = {A lambda calculus for quantum computation with classical control}, volume = {16}, issn = {1469-8072, 0960-1295}, url = {http://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/lambda-calculus-for-quantum-computation-with-classical-control/53AB540D33E2E420DF2F28D0073B7F45}, doi = {10/cb9gnr}, abstract = {In this paper we develop a functional programming language for quantum computers by extending the simply-typed lambda calculus with quantum types and operations. The design of this language adheres to the ‘quantum data, classical control’ paradigm, following the first author's work on quantum flow-charts. We define a call-by-value operational semantics, and give a type system using affine intuitionistic linear logic. The main results of this paper are the safety properties of the language and the development of a type inference algorithm.}, language = {en}, number = {3}, urldate = {2019-10-26}, journal = {Mathematical Structures in Computer Science}, author = {Selinger, Peter and Valiron, Benoit}, month = jun, year = {2006}, note = {ZSCC: 0000136}, pages = {527--552} }

Downloads: 0