A Quantum-Control Lambda-Calculus with Multiple Measurement Bases
arXiv:2506.16244 · doi:10.1007/978-981-95-3585-9_8
Abstract
We introduce Lambda-SX, a typed quantum lambda-calculus that supports multiple measurement bases. By tracking duplicability relative to arbitrary bases within the type system, Lambda-SX enables more flexible control and compositional reasoning about measurements. We formalise its syntax, typing rules, subtyping, and operational semantics, and establish its key meta-theoretical properties. This proof-of-concept shows that support for multiple bases can be coherently integrated into the type discipline of quantum programming languages.
arXiv commentThis includes the appendix that was omitted from the APLAS 2025 publication
References in corpus (13)
- Quipper: A Scalable Quantum Programming Language
- A functional quantum programming language
- Lineal: A linear-algebraic Lambda-calculus
- Call-by-value, call-by-name and the vectorial behaviour of the algebraic λ-calculus
- Two linearities for quantum computing in the lambda calculus
- Realizability in the Unitary Sphere
- Quantum Control in the Unitary Sphere: Lambda-S1 and its Categorical Model
- A categorical construction for the computational definition of vector spaces
- A linear linear lambda-calculus
- A concrete model for a typed linear algebraic lambda calculus
- Towards a Computational Quantum Logic: An Overview of an Ongoing Research Program
- The Quantum Effect: A Recipe for QuantumPi
- The Many-Worlds Calculus