A Lambda Calculus for Quantum Computation with Classical Control

The objective of this paper is to develop a functional programming language for quantum computers. We develop a lambda calculus for the classical control model, following the first author’s work on quantum flow-charts. We define a call-by-value operational semantics, and we 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.

• Type: Conference
• Year: 2005
• Where: TLCA
• Authors: Peter Selinger, Benoît Valiron
• Keywords: Call-by-value Operational Semantics, Functional Programming Language, Theoretical Computer Science, TLCA 2005, Type Inference Algorithm