A lambda calculus for quantum computation with classical control
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.(Published Online July 4 2006)
(Received April 18 2005)
(Revised December 15 2005)
1 Research supported by NSERC.