Relational Proofs for Quantum Programs

Paper information (formal volume: 2020, POPL/PACMPL 4; published online: December 2019) — Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, and Li Zhou. DOI; arXiv:1901.05184

Work

The paper proposes a relational logic for quantum programs based on a quantum analogue of probabilistic couplings. Relational proofs concern two executions or programs together, rather than only a single program's postcondition. The authors apply the logic to uniformity of a quantum Bernoulli factory, noisy teleportation, the quantum one-time pad, and quantum walks.

Contributions

• A quantum relational-proof logic grounded in quantum couplings.
• Expressions for cross-program equivalence, reliability, and cryptographic security.
• Verification of quantum Bernoulli-factory sample uniformity, teleportation reliability under bit- and phase-flip noise, quantum one-time-pad security, and equivalence of quantum walks.
• An extension of probabilistic relational reasoning to quantum states and processes.

Limits

Relational proofs depend on coupling constructions, relational predicates, and the chosen quantum semantics; successful examples do not make arbitrary relational properties automatic. Noise, measurement outcomes, and open-system boundaries must be modeled explicitly, and the logic does not replace hardware certification or resource-performance analysis.

Connections

The paper belongs to the relational-verification line of Quantum Relational Hoare Logic and can be contrasted with the single-program assertions of Floyd–Hoare Logic for Quantum Programs. Compared with Bisimulation for Quantum Processes, it emphasizes couplings and relational predicates, while bisimulation emphasizes behavioral process equivalence.

Original paper

Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, and Li Zhou, Relational Proofs for Quantum Programs, Proceedings of the ACM on Programming Languages 4(POPL), Article 21 (2020), DOI: 10.1145/3371089. arXiv:1901.05184