Relational Proofs For Quantum Programs | Awesome Quantum Computing Papers

Relational Proofs For Quantum Programs

Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, Li Zhou Β· Proceedings of the ACM on Programming Languages Β· 2019

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.

Explore more on:
Quantum Algorithms
Similar Work
Loading…