Invited talk: Twist: Sound Reasoning for Purity and Entanglement in Quantum P...
summary
Twist is a quantum language that encodes a type system for purity so programs can assert lack of entanglement and have those assertions checked by a mix of static analysis and runtime verification. It implements cast and split assertions, uses backwards entanglement propagation statically and SVD in simulation or an iterated swap test on hardware to verify separability, expresses Grover/QFT/error‑correction, catches injected bugs, and reports runtime overhead under 3.5% (with one case where static checks are conservative).
AI-written summary · about
chapters (19)
- 0:00Start
- 0:44Quantum Programming
- 1:51A Subtle Bug
- 2:51Finding the Bug
- 3:31Quantum Entanglement
- 4:10Fixing the Entanglement Bug
- 9:37Measurement
- 12:11The Bug, Revisited
- 13:42Types Specify Purity
- 15:39Operators Assert Purity
- 17:39Static Analysis Verifies cast
- 18:47Dynamic Test Verifies split
- 19:08Runtime Separability Test
- 20:44Evaluation Questions
- 21:21Twist Analysis Results
- 24:14Runtime Verification Overhead
- 27:34Mixed vs. Pure State Simulation
- 28:45Looking Forward
- 42:09Classical Control Flow
related talks
20mTwist: Sound Reasoning for Purity and Entanglement in Quantum Programs
15mToward A Quantum Programming Language for Higher Level Formal Verification
42mQuantum program analysis: Verification and Testing
25mA Static Analysis of Entanglement
01h 01mInvited Talk: Welcome to Quantum 3.0!
13mQbC: Quantum Correctness by Construction
19mA Static Analysis for High-Level Quantum Programming Languages
22mEfficient Formal Verification of Quantum Error Correcting Programs