A lambda calculus for quantum computation with classical control

TL;DR

This paper introduces a lambda calculus tailored for quantum computation with classical control, providing a formal foundation, operational semantics, and a type system to ensure safety and facilitate implementation.

Contribution

It presents a novel lambda calculus for quantum programming with classical control, including semantics, a type system, and a type inference algorithm.

Findings

Proved safety properties of the language

Developed a type inference algorithm

Established a formal operational semantics

Abstract

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.