Hostname: page-component-78c5997874-dh8gc Total loading time: 0 Render date: 2024-11-08T05:04:25.929Z Has data issue: false hasContentIssue false
  • English
  • Français

A lambda calculus for quantum computation with classical control

Published online by Cambridge University Press:  04 July 2006

PETER SELINGER  and
BENOIT VALIRON
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
Get access Rights & Permissions [Opens in a new window]

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.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 16 , Issue 3 , June 2006 , pp. 527 - 552
Copyright
2006 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)