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.

@article{paperbot558,
  title = {Relational proofs for quantum programs},
  author = {Gilles Barthe and Justin Hsu and Mingsheng Ying and Nengkun Yu and Li Zhou},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {4},
  number = {POPL},
  year = {2019},
  doi = {10.1145/3371089}
}