Tracking Errors through Types in Quantum Programs
summary
A type extension records a natural-number k errors on each qubit and a gate annotation for how many errors it adds; implemented in the embedded quantum language choir on the kakapo Phasis net. Type checking enforces the arithmetic constraint K + sum(inputs) < T so well-typed circuits are fault tolerant up to threshold T. The implementation typechecks and infers types for examples including a teleportation circuit where intermediate gates create two errors and the threshold is three.
AI-written summary · about
chapters (12)
- 0:00Intro
- 0:12Overview
- 0:56QWIRE
- 2:33Wire Types
- 3:34What kind of Qubit?
- 4:59Adding Errors
- 5:36Error Prone Gates
- 8:15Error Correction Gates
- 8:55Checking Fault Tolerance
- 9:45Typechecking
- 12:20Type Inference
- 13:03Questions
related talks
28mA type-theoretic account of quantum computation (Extended Abstract)
22mQbC: Quantum Correctness by Construction
30mOn incorrectness logic for Quantum programs
29mEfficiently Verifying Quantum Programs with Few T Gates
16mExtending Gottesman Types Beyond the Clifford Group
01h 01mInvited Talk: Welcome to Quantum 3.0!
19mAvenues for Quantum Error Correction and Mitigation
22mEfficient Formal Verification of Quantum Error Correcting Programs