A feasible and unitary programming language with quantum control
summary
Defines PUNQ, a typed quantum lambda calculus that enforces polynomial-time normalization and enforces unitarity via orthogonality by using a modality for superpositions plus a linear-logic type discipline (Barber–Plotkin duality) to prevent duplications. Proves subject reduction and shows soundness/completeness for fixed-dimension n→k isometries (unitary when n=k) and gives a compilation to polynomial-size circuits. Open: full quantum-polynomial-time completeness with polymorphic lists and orthogonality remains unresolved.
AI-written summary · about
chapters (8)
- 0:00Quantum polynomial time intro
- 3:07Compiling to quantum circuits
- 7:23PUN programming language
- 10:37Typing rules in PUN
- 13:50Linear vs nonlinear typing
- 17:18Qubit list challenges
- 19:12Fixed-dimension unitaries
- 20:28Q&A on linearity
related talks
24mQunity: A Unified Language for Quantum and Classical Computing
26mQudit Quantum Programming with Projective Cliffords
15mToward A Quantum Programming Language for Higher Level Formal Verification
30mQuantum Computing for Programming Languages Researchers
28mA type-theoretic account of quantum computation (Extended Abstract)
21mInteractive Proofs for Synthesizing Quantum States and Unitaries
21mToward Certified Quantum Programming
30mDependently Typed Quantum Programming in Proto-Quipper