lambda calculus

Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages

We introduce a type system for the Quipper language designed to derive upper bounds on the size of the circuits produced by the typed program. This size can be measured according to various metrics, including width, depth and gate count, but also …

Two linearities for quantum computing in the lambda calculus

We propose a way to unify two approaches of non-cloning in quantum lambda-calculi: logical and algebraic linearities. The first approach is to forbid duplicating variables, while the second is to consider all lambda-terms as algebraic-linear …

Realizability in the Unitary Sphere

In this paper we present a semantics for a linear algebraic lambda-calculus based on realizability. This semantics characterizes a notion of unitarity in the system, answering a long standing issue. We derive from the semantics a set of typing rules …

A Lambda Calculus for Density Matrices with Classical and Probabilistic Controls

In this paper we present two flavors of a quantum extension to the lambda calculus. The first one, 𝜆𝜌, follows the approach of classical control/quantum data, where the quantum data is represented by density matrices. We provide an interpretation for …

Typing Quantum Superpositions and Measurement

We propose a way to unify two approaches of non-cloning in quantum lambda-calculi. The first approach is to forbid duplicating variables, while the second is to consider all lambda-terms as algebraic-linear functions. We illustrate this idea by …

The Geometry of Parallelism: Classical, Probabilistic, and Quantum Effects

We introduce a Geometry of Interaction model for higher-order quantum computation, and prove its adequacy for a fully fledged quantum programming language in which entanglement, duplication, and recursion are all available. This model is an instance …

Physics, Topology, Logic and Computation: A Rosetta Stone

In physics, Feynman diagrams are used to reason about quantum processes. In the 1980s, it became clear that underlying these diagrams is a powerful analogy between quantum physics and topology. Namely, a linear operator behaves very much like a …

The Arrow Calculus as a Quantum Programming Language

We express quantum computations (with measurements) using the arrow calculus extended with monadic constructions. This framework expresses quantum programming using well-understood and familiar classical patterns for programming in the presence of …

A Brief Survey of Quantum Programming Languages

This article is a brief and subjective survey of quantum programming language research.