一句话：提出基于量子耦合的关系程序逻辑，用于验证量子程序的关系性质。
本文面向量子程序的关系验证问题，提出一种关系程序逻辑。其语义解释建立在概率耦合的量子类似物之上，从而能够统一刻画两个量子程序之间的关联行为。作者利用该逻辑验证了若干非平凡关系性质，包括量子伯努利工厂所生成样本的均匀性、量子隐形传态在比特翻转与相位翻转噪声下的可靠性、量子一次性密码本的安全性，以及量子行走的等价性。结果表明，耦合式关系推理可有效支持量子与后量子安全等领域中的验证任务。
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}
}