Mathematical Structures in Computer Science



Paper

A lambda calculus for quantum computation with classical control


PETER SELINGER a1 1 and BENOIT VALIRON a2
a1 Department of Mathematics and Statistics, Dalhousie University, Halifax, Nova Scotia, Canada
a2 Department of Mathematics and Statistics, University of Ottawa, Ottawa, Ontario, Canada

Article author query
selinger p   [Google Scholar] 
valiron b   [Google Scholar] 
 

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.

(Published Online July 4 2006)
(Received April 18 2005)
(Revised December 15 2005)



Footnotes

1 Research supported by NSERC.