A Static Analysis for High-Level Quantum Programming Languages
summary
A static analysis that builds a control‑flow graph and runs a backward safe/unsafe liveness pass identifies temporaries that must be explicitly discarded and automatically inserts the discard calls. A prototype is implemented inside the Goopy prototype compiler and successfully fixes simple examples that would otherwise be linear‑type errors, but it does not detect entanglement and can produce unsafe early discards there. Future work adds entanglement and classical analyses to reduce unnecessary discards and improve precision.
AI-written summary · about
chapters (12)
- 0:00Quantum programming challenges
- 1:11Linear types for quantum variables
- 3:19Limitations of linear types
- 4:05Static analysis for discarding
- 5:07Control flow graph
- 6:28Liveness analysis for quantum variables
- 9:41Inserting discard functions
- 12:38Relaxing type systems
- 13:20Implementation in Goopy
- 14:46Future improvements
- 17:12Entanglement and compiler integration
- 19:00Q&A
related talks
15mToward A Quantum Programming Language for Higher Level Formal Verification
30mDependently Typed Quantum Programming in Proto-Quipper
24mQuantum Control Machine: The Limits of Control Flow in Quantum Programming
30mOn incorrectness logic for Quantum programs
13mQbC: Quantum Correctness by Construction
25mA Static Analysis of Entanglement
16mProjection-Based Runtime Assertions for Testing and Debugging Quantum Programs
22mQuantum Controlled Measurements via Program Transformation