Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs
summary
Proposes a new quantum Hoare logic that handles hybrid classical–quantum imperative programs by modeling program states as partial density operator value distributions and specifying probabilistic outcomes with distribution formulas. Proves soundness against a denotational semantics, gives a frame rule for local reasoning across measurements and unbounded while loops, and mechanically sketches proofs of nontrivial algorithms, including formal correctness outlines for HHL and Shor’s algorithm. Reports manual proofs and ongoing work toward interactive formalization.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:03Language design and semantics
- 3:51Operational semantics
- 7:03Denotational semantics
- 9:10Quantum program logic
- 13:53Inference rules: classical
- 15:29Inference rules: quantum
- 17:19Soundness theorem
- 18:05Case study: simple program
- 18:26Case study: HHL algorithm
- 19:08Conclusion
- 19:50Q&A
related talks
42mQuantum program analysis: Verification and Testing
35mQuantum relational Hoare logic, towards a formalization
30mOn incorrectness logic for Quantum programs
20mA Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantu
13mQbC: Quantum Correctness by Construction
27mAn Expressive Assertion Language for Quantum Programs
18mConcurrent Quantum Separation Logic for Fine-Grained Parallelism
22mQbC: Quantum Correctness by Construction