Relational proofs for quantum programs

作     者：Barthe, Gilles Hsu, Justin Ying, Mingsheng Yu, Nengkun Zhou, Li 

作者机构：Max Planck Institute for Security and Privacy Germany IMDEA Software Institute Spain Department of Computer Sciences University of Wisconsin-Madison United States Centre for Quantum Software and Information University of Technology Sydney Australia State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences China Tsinghua University China Centre for Quantum Software and Information University of Technology Sydney Australia Max Planck Institute for Security and Privacy Germany Department of Computer Science and Technology Tsinghua University China 

出 版 物：《arXiv》 (arXiv)

年 卷 期：2019年

核心收录：

主　　题：Application programs 

摘      要：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. Copyright © 2019, The Authors. All rights reserved.