A type-theoretic account of quantum computation (Extended Abstract)
summary
Provides a Coq encoding of pure quantum circuits that represents states as functions and transformations as parametric, natural linear maps, requires proving naturality for unitary morphisms, and implements lenses and currying to focus gates on subsets of wires. Builds compositional focusing that preserves composition and unitarity, then mechanizes short proofs: the 9‑qubit error‑correction encoder/decoder composes to the identity on the encoded basis (proof sketched in 18 lines), plus GHZ state preparation and a reverse circuit, all verified in Coq.
AI-written summary · about
chapters (6)
- 0:00Introduction
- 1:19Unitary semantics
- 9:58Compositionality challenges
- 16:05Direct power vector space
- 21:07Circuit correctness with lenses
- 25:44Conclusion
related talks
22mCoqQ: Foundational Verification of Quantum Programs
22mQbC: Quantum Correctness by Construction
01h 01mWhat Is "Quantum" About Quantum Computing?
21mQuantum and Classical Control (work-in-progress)
49mQuantum Garbled Circuits
15mToward A Quantum Programming Language for Higher Level Formal Verification
13mQbC: Quantum Correctness by Construction
23mA feasible and unitary programming language with quantum control