Denotational semantics for stabiliser quantum programs
summary
Claims a sound, universal and complete denotational semantics for stabiliser operations that includes measurement, classical control and quantum error‑correcting codes as first‑class objects, interpreting operations as affine relations (with a symplectic modality). Provides a proof‑of‑concept assembly language with an implemented semantics that is fully-abstract denotational semantics, and shows equivalence to trace‑preserving mixed stabiliser operations and the syntax. Limits: works for odd prime dimensions (qubits need phase gates), only linear classical control, AND left as a conjecture.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:47Need for stabilizer programming
- 3:55Stabilizer theory foundations
- 5:21Stabilizer states as affine subspaces
- 7:07Stabilizer operations as relations
- 8:33Measurements and corrections
- 10:22Denotational semantics
- 12:06Limitations and future work
- 13:53Conclusion
related talks
24mSemantics for Variational Quantum Programming
22mA Semantics for Quantum Loops
21mQuantum and Classical Control (work-in-progress)
30mQuantum Computing for Programming Languages Researchers
30mOn incorrectness logic for Quantum programs
42mQuantum program analysis: Verification and Testing
13mQbC: Quantum Correctness by Construction
18mFormalization of a Programming Language for Quantum Circuits with Measurement and Classical Control