A lambda calculus for quantum computation with classical control

• Autores: Peter Selinger, Benoit Valiron
• Localización: Mathematical structures in computer science, ISSN 0960-1295, Vol. 16, Nº 3, 2006, págs. 527-552
• Idioma: inglés
• DOI: 10.1017/s0960129506005238
• Texto completo no disponible (Saber más ...)
• Resumen

  • 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.