Quantum relational Hoare logic, towards a formalization
summary
Quantum relational Hoare logic (qRHL) formalizes relationships between two quantum programs by interpreting pre/postconditions as subspaces of joint memory and requiring resulting marginals come from a separable joint state, which fixes a counterintuitive equality rule. A prototype tool emits verification conditions handled by Isabelle/HOL and proves one nontrivial post‑quantum crypto proof; core formalization work builds an Isabelle library for Hilbert spaces, tensor products and trace‑class operators, while semantics and full proof rules remain to be encoded.
AI-written summary · about
chapters (7)
- 0:00Intro
- 0:23Overview
- 4:48Relational Hoare Logic (RHL)
- 8:09Quantum Relational Hoare Logic (qRHL)
- 12:21Specific Challenges
- 21:47Challenge: representing assertions
- 31:39Register formalism
related talks
22mLocal Reasoning about Probabilistic Behaviour for Classical-Quantum Programs
42mQuantum program analysis: Verification and Testing
20mA Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantu
22mCoqQ: Foundational Verification of Quantum Programs
23mAutomating Quantum Hoare Logic with Automata (Work-In-Progress)
13mQbC: Quantum Correctness by Construction
27mAn Expressive Assertion Language for Quantum Programs
18mConcurrent Quantum Separation Logic for Fine-Grained Parallelism