A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantu
summary
Proposes a Hoare-style logic that gives a quantum separating conjunction and a quantum frame rule so local reasoning carries over when multi-qubit states factorize. Mixed states are represented as weighted pure states to let predicates split by tensor-factorization; entangled states fail this and are excluded. Provides operational semantics for allocation, unitary and measurement statements and verifies Deutsch–Jozsa and Grover examples end-to-end, but stops short of full automation or handling general entanglement.
AI-written summary · about
chapters (13)
- 0:00Intro
- 1:13Quantum programs: Example
- 3:02Superposition
- 4:49Programming language
- 6:25A simpler representation
- 7:38Transformation: Example
- 8:40Measurement: Example
- 9:06Quantum rules
- 9:25Frame rule
- 11:17Factorization for local reasoning
- 13:14Quantum heaps
- 13:58Example: Deutsch's algorithm
- 17:04Conclusion
related talks
18mConcurrent Quantum Separation Logic for Fine-Grained Parallelism
22mLocal Reasoning about Probabilistic Behaviour for Classical-Quantum Programs
35mQuantum relational Hoare logic, towards a formalization
16mQ*: Implementing Quantum Separation Logic in F*
42mQuantum program analysis: Verification and Testing
18mSAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum(…)
28mA type-theoretic account of quantum computation (Extended Abstract)
22mQbC: Quantum Correctness by Construction