A Quantum-Control Lambda-Calculus with Multiple Measurement Bases
Alejandro D\'iaz-Caro, Nicolas A. Monzon
TL;DR
This paper presents Lambda-SX, a typed quantum lambda-calculus supporting multiple measurement bases, enabling flexible measurement control and compositional reasoning within quantum programming languages.
Contribution
It introduces Lambda-SX, a novel calculus that integrates multiple measurement bases into the type system of quantum programming languages.
Findings
Formal syntax, typing rules, and semantics established
Supports arbitrary measurement bases within type discipline
Proven meta-theoretical properties of the calculus
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsQuantum Computing Algorithms and Architecture · Logic, Reasoning, and Knowledge · Logic, programming, and type systems