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.
This includes the appendix that was omitted from the APLAS 2025 publication