RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing
summary
RapunSL presents a program logic that adds linear combination (scalar multiply and plus) and a separate mixing connective to quantum separation logic, so superposition and measurement reduce to reasoning about pure states. It proves three localities—entanglement-locality via separation, basis-locality via scalars/sums, and outcome-locality via mixing—and verifies case studies including teleportation, CNOT-by-measurement, an algorithm using ~30 qubits, and the bit‑flip error‑correction circuit. Limits include an unavoidable 2^n branching after n measurements, though manual proofs often avoid blowup.
AI-written summary · about
chapters (11)
- 0:00Introduction to RapunSL and quantum separation logic
- 1:23Quantum separation logic limits
- 5:21Linear structure in RapunSL
- 7:49Basis locality simplification
- 9:14Handling measurement
- 11:00New connectives in RapunSL
- 12:25Trade-offs with measurements
- 15:18Error correction case study
- 17:47Comparison with prior work
- 18:53Conclusion
- 19:15Q&A
related talks
27mScheme Pearl: Quantum Continuations
30mSymbolic Execution of Hadamard-Toffoli Quantum Circuits
25mExponential separations using guarded extension variables
15mProgramming and Reasoning with Partial Observability
35mSQUIP or Why We Need to Study Processors Like Nature
26mWhile(1) i++ — How far can it go?
25mBit Complexity of Jordan Normal Form and Spectral Factorization
23mMatrix multiplication via matrix groups