Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime
summary
Extends Rust’s type system with sharp α types so qubits are lifetime-annotated dropable qubits (affine inside a lifetime, linear outside), gives two operational semantics — a mathematical simulation semantics and a circuit-building pebble-game circuit semantics — and proves they coincide; shows automatic uncomputation is decidable under a classical-circuit restriction and type-checks nontrivial examples including Grover; prototype remains theoretical (no production compiler/simulator yet).
AI-written summary · about
chapters (9)
- 0:00Qurts and quantum computation
- 2:37Linear types in quantum programming
- 6:07Automatic uncomputation need
- 8:17Lifetimes for uncomputation
- 11:48Temporal drop semantics with lifetimes
- 13:13Uncomputation semantics: simulation and pebble games
- 14:18Prior work on automatic uncomputation
- 15:21Summary and future
- 15:43Q&A
related talks
17mToward a Type Theoretic Interpretation of Q# and Statically Enforcing the No Cloning Theorem
28mA type-theoretic account of quantum computation (Extended Abstract)
24mQunity: A Unified Language for Quantum and Classical Computing
30mDependently Typed Quantum Programming in Proto-Quipper
22mQbC: Quantum Correctness by Construction
15mAssertion-Based Optimization of Quantum Programs
15mToward A Quantum Programming Language for Higher Level Formal Verification
40mQ# - going beyond quantum circuits