Toward a Type Theoretic Interpretation of Q# and Statically Enforcing the No Cloning Theorem
summary
Formal definition of Q# via a core calculus lambda qsharp models qubits as opaque symbols and surface qubits as qref references, introduces lifetime variables κ and a dagger κ type that blocks a qubit until its lifetime ends, and adds borrowing/reborrowing rules (Rust-like) that statically reject cloning like using the same qubit as control and target for CNOT. Mechanization uses art and lngen, work extends to measurement, polymorphism, and QIR/QMLIR compilation.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 1:12Why Formalize Languages
- 3:43Features of Q
- 4:52Sample Program
- 5:29Formal Specification
- 6:51lambda calculus
- 8:39commands
- 10:04example
- 11:09typing context evolution
- 13:29typing rules
- 15:03formalization
- 16:01future steps
- 16:45summary
related talks
21mQurts: Automatic Quantum Uncomputation by Affine Types with Lifetime
40mQ# - going beyond quantum circuits
35mQuantum relational Hoare logic, towards a formalization
22mQbC: Quantum Correctness by Construction
28mA type-theoretic account of quantum computation (Extended Abstract)
13mQbC: Quantum Correctness by Construction
21mQuantum and Classical Control (work-in-progress)
22mCoqQ: Foundational Verification of Quantum Programs