Relational proofs for quantum programs
- Publication Type:
- Journal Article
- Citation:
- Proceedings of the ACM on Programming Languages, 2020, 4, (POPL), pp. 21:1-21:1
- Issue Date:
- 2020-01-01
Closed Access
Filename | Description | Size | |||
---|---|---|---|---|---|
Relational_Proofs_for_Quantum_Programs.pdf | Published version | 924.78 kB |
Copyright Clearance Process
- Recently Added
- In Progress
- Closed Access
This item is closed access and not available.
© 2020 Copyright held by the owner/author(s). 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.
Please use this identifier to cite or link to this item: