Hostname: page-component-6bf8c574d5-gr6zb Total loading time: 0 Render date: 2025-02-21T00:12:57.584Z Has data issue: false hasContentIssue false

A lambda calculus for quantum computation with classical control

Published online by Cambridge University Press:  04 July 2006

PETER SELINGER
Affiliation:
Department of Mathematics and Statistics, Dalhousie University, Halifax, Nova Scotia, Canada
BENOIT VALIRON
Affiliation:
Department of Mathematics and Statistics, University of Ottawa, Ottawa, Ontario, Canada
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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.

Type
Paper
Copyright
2006 Cambridge University Press