We study a measurement-free, untyped λ-calculus with quantum data and classical control. This work arises from previous proposals by Selinger and Valiron, and Van Tonder. We focus on operational and expressiveness issues, rather than (denotational) semantics. We prove subject reduction and confluence, and a standardisation theorem. Moreover, we prove the computational equivalence of the proposed calculus with a suitable class of quantum circuit families.

Mathematical Structures in Computer ScienceFeb 16, 200920 citations

arXiv:2506.16244 · Lecture notes in computer science

A Quantum-Control Lambda-Calculus with Multiple Measurement Bases

Alejandro Díaz-Caro, Nicolas A. Monzon

Published Oct 30, 2025• 0 citations

arXiv HTML PDF

DOI: 10.1007/978-981-95-3585-9_8

Related papers

A fully abstract model for quantum controlled lambda calculus

Alejandro Díaz-Caro, Octavio Malherbe

Jun 1, 20181 citation

A Lambda Calculus for Quantum Computation with Classical Control

Peter Selinger, Benoît Valiron

arXiv:cs/0404056Lecture notes in computer scienceJan 1, 200534 citations

Two linearities for quantum computing in the lambda calculus

Alejandro Díaz-Caro, Gilles Dowek B, Juan Pablo Rinaldi

arXiv:1601.04294BiosystemsNov 19, 201918 citations

A Double Effect λ-calculus for Quantum Computation

Juliana Kaizer Vizzotto, Bruno Crestani Calegaro, Eduardo Kessler Piveta

Lecture notes in computer scienceJan 1, 20136 citations

A concrete model for a typed linear algebraic lambda calculus

Alejandro Díaz-Caro, Octavio Malherbe

Abstract We give an adequate, concrete, categorical-based model for Lambda- ${\mathcal S}$ , which is a typed version of a linear-algebraic lambda calculus, extended with measurements. Lambda- ${\mathcal S}$ is an extension to first-order lambda calculus unifying two approaches of non-cloning in quantum lambda-calculi: to forbid duplication of variables and to consider all lambda-terms as algebraic linear functions. The type system of Lambda- ${\mathcal S}$ has a superposition constructor S such that a type A is considered as the base of a vector space, while SA is its span. Our model considers S as the composition of two functors in an adjunction relation between the category of sets and the category of vector spaces over $\mathbb C$ . The right adjoint is a forgetful functor U, which is hidden in the language, and plays a central role in the computational reasoning.Abstract We give an adequate, concrete, categorical-based model for Lambda- ${\mathcal S}$ , which is a typed version of a linear-algebraic lambda calculus, extended with measurements. Lambda- ${\mathcal S}$ is an extension to first-order lambda calculus unifying two approaches of non-cloning in quantum lambda-calculi: to forbid duplication of variables and to consider all lambda-terms as algebraic linear functions. The type system of Lambda- ${\mathcal S}$ has a superposition constructor S such that a type A is considered as the base of a vector space, while SA is its span. Our model considers S as the composition of two functors in an adjunction relation between the category of sets and the category of vector spaces over $\mathbb C$ . The right adjoint is a forgetful functor U, which is hidden in the language, and plays a central role in the computational reasoning.

arXiv:1806.09236Mathematical Structures in Computer ScienceNov 21, 20234 citations

On a measurement-free quantum lambda calculus with classical control

Ugo Dal Lago, Andrea Masini, Margherita Zorzi

Mathematical Structures in Computer ScienceFeb 16, 200920 citations

Abstract We give an adequate, concrete, categorical-based model for Lambda-

{\mathcal S}

, which is a typed version of a linear-algebraic lambda calculus, extended with measurements. Lambda-

{\mathcal S}

is an extension to first-order lambda calculus unifying two approaches of non-cloning in quantum lambda-calculi: to forbid duplication of variables and to consider all lambda-terms as algebraic linear functions. The type system of Lambda-

{\mathcal S}

has a superposition constructor S such that a type A is considered as the base of a vector space, while SA is its span. Our model considers S as the composition of two functors in an adjunction relation between the category of sets and the category of vector spaces over

\mathbb C

. The right adjoint is a forgetful functor U, which is hidden in the language, and plays a central role in the computational reasoning.