Quantum Relational Hoare Logic
Quantum Relational Hoare Logic
Unruh introduces relational Hoare logic for comparing quantum programs and analyzing quantum-cryptographic protocols.
Paper information (2019, POPL/PACMPL) — Dominique Unruh. DOI; author page; preprint
Work
Quantum relational Hoare logic (qRHL) reasons about pairs of imperative quantum programs: if their inputs satisfy a relation, do their outputs satisfy the corresponding relation? It follows the security-proof style of probabilistic relational Hoare logic while addressing quantum-register equality, measurement, and quantum cryptographic protocols. The paper also implements a proof tool and develops security examples.
Contributions
- A relational Hoare logic for quantum programs.
- A treatment of relational predicates over quantum registers and paired executions.
- Applications to post-quantum cryptography and quantum-protocol security.
- A qRHL proof tool and example security proofs.
Limits
Results depend on relational predicates, the program model, and the semantic assumptions behind the rules; tool support does not make every property automatically provable. The logic focuses on relational and security properties and does not directly provide hardware-noise, performance, or single-program functional guarantees for all inputs.
Connections
Inspired by probabilistic relational Hoare logic, qRHL can be contrasted with the single-program assertions of Floyd–Hoare Logic for Quantum Programs. This comparison does not assert a direct extension of Ying's proof system. It complements Relational Proofs for Quantum Programs. Compared with Communicating Quantum Processes, qRHL centers relational specifications and security proofs rather than process-communication semantics.
Original paper
Dominique Unruh, Quantum Relational Hoare Logic, Proceedings of the ACM on Programming Languages 3(POPL), Article 33 (2019), DOI: 10.1145/3290346. Author page