Dependently Typed Quantum Programming in Proto-Quipper
summary
Proto-Quipper claims a practical, type-safe fix for Quipper’s unsoundness by adding dependent linear types that force a shape/parameter separation (types only depend on shapes like list lengths, not quantum state), with formal operational and denotational semantics and a proof of type safety. An implementation (a linear-Agda-like system) exists, generates circuits of millions of gates, supports boxing/unboxing of circuits, omits full classical feedback and heavy optimizers, and works as described.
AI-written summary · about
chapters (8)
- 0:00Quantum programming challenges
- 1:28The Quire programming language
- 4:24Circuits as first-class objects
- 7:16Boxing and unboxing circuits
- 10:48Parameters versus states
- 13:52Limitations of current systems
- 18:32Linear dependent types
- 24:56Feedback and optimization Q&A
related talks
20mProto-Quipper with Dynamic Lifting
17mEncoding High-level Quantum Programs as SZX-diagrams
19mFlexible Type-Based Resource Estimation in Quantum Circuit Description Languages
18mType-safe (Variational) Quantum Programming in Idris
15mToward A Quantum Programming Language for Higher Level Formal Verification
23mA feasible and unitary programming language with quantum control
13mQbC: Quantum Correctness by Construction
21mQurts: Automatic Quantum Uncomputation by Affine Types with Lifetime