Extending Gottesman Types Beyond the Clifford Group
summary
Extends Gottesman-style types from Clifford-only to universal circuits by adding intersection types plus numeric additive types so T and arbitrary 1‑qubit unitaries get literal type expressions; introduces a normalized row‑echelon form for types to detect separability and to type measurement outcomes; shows T† can be expressed as seven T gates and derives its type, types a Toffoli decomposition to prove it acts classically on three Z qubits, and demonstrates magic-state injection that yields ax+by typed outputs.
AI-written summary · about
chapters (11)
- 0:00Intro
- 0:19What types?
- 1:40Too Many Types?
- 2:22Inspecting CNOT
- 4:46What's Missing?
- 5:57Normalization
- 8:37Measurement
- 9:26Adding T
- 12:36Typing Toffoli
- 13:50Gate Injection
- 15:00Next Steps
related talks
24mAdventures in Qutrit Compilation
28mA type-theoretic account of quantum computation (Extended Abstract)
29mEfficiently Verifying Quantum Programs with Few T Gates
22mTopological Quantum Programming in TED-K
16mTracking Errors through Types in Quantum Programs
58mBosonic (And Other) Codes With Interesting Logical Gate Sets
22mOptimal Two-Qubit Circuits for Universal Fault-Tolerant Quantum Computation
20mTowards a Hierarchical Quantum Circuit Language