Relational Proofs for Quantum Programs

Abstract

Relational verification of quantum programs has many potential applications in quantum and post-quantum security and other domains. We propose a relational program logic for quantum programs. The interpretation of our logic is based on a quantum analogue of probabilistic couplings. We use our logic to verify non-trivial relational properties of quantum programs, including uniformity for samples generated by the quantum Bernoulli factory, reliability of quantum teleportation against noise (bit and phase flip), security of quantum one-time pad and equivalence of quantum walks.

34 pages, LaTeX; v2: extend version of conference paper

References in corpus (8)

• Quantum random walks - an introductory overview
• Quantum walks: a comprehensive review
• Optimal Encryption of Quantum Bits
• Tight uniform continuity bounds for quantum entropies: conditional entropy, relative entropy distance and energy constraints
• Proving Differential Privacy via Probabilistic Couplings
• Quantum Relational Hoare Logic
• Relational reasoning via probabilistic coupling
• Proving Expected Sensitivity of Probabilistic Programs

Cited by in corpus (7)

• Quantum Hoare logic with classical variables
• Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
• Efficient Formal Verification of Quantum Error Correcting Programs
• Algebraic Reasoning of Quantum Programs via Non-idempotent Kleene Algebra
• On Algebraic Abstractions for Concurrent Separation Logics
• Automating Equational Proofs in Dirac Notation
• A Practical Quantum Hoare Logic with Classical Variables, I