Concurrent Quantum Separation Logic for Fine-Grained Parallelism
summary
Introduces a concurrent quantum separation logic that verifies fine-grained parallel quantum code, with a concrete linear combination of Hoare triples rule to reason about superpositions and a fractional token scheme plus a cubit token to share qubits safely; adds an anti-frame rule to promote partial ownership to full ownership at atomic steps. Shows mechanized proofs of a nontrivial parallelized circuit (including arbitrary commuting matrices) and sketches an extension to density-matrix probabilistic reasoning via a convex PCM.
AI-written summary · about
chapters (10)
- 0:00Concurrent quantum separation logic
- 1:51Quantum computing basics
- 3:39Motivation for parallelizing
- 5:05Target language and logic
- 6:55Example and race conditions
- 8:48Linear combination rule
- 11:56Parallelizing commuting matrices
- 12:17Logic for probabilistic reasoning
- 14:23Conclusion and future work
- 14:45Q&A: Loop rules and entanglement
related talks
20mA Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantu
16mQ*: Implementing Quantum Separation Logic in F*
42mQuantum program analysis: Verification and Testing
22mLocal Reasoning about Probabilistic Behaviour for Classical-Quantum Programs
35mQuantum relational Hoare logic, towards a formalization
13mQbC: Quantum Correctness by Construction
18mSAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum(…)
15mToward A Quantum Programming Language for Higher Level Formal Verification