论文标题
证明量子程序正确
Proving Quantum Programs Correct
论文作者
论文摘要
随着量子计算从理论稳步发展，程序员将面临一个共同的问题：他们如何确定他们的代码可以执行其打算做的事情？本文提出了令人鼓舞的结果，导致在SQIR开发的背景下将机械化证明应用于量子编程领域。它验证了一系列量子算法的正确性，包括Grover的算法和量子相估计，这是Shor算法的关键组成部分。在此过程中，它旨在突出量子环境中形式验证的成功和挑战，并激发定理证明社区将量子计算作为应用领域的目标。
As quantum computing progresses steadily from theory into practice, programmers will face a common problem: How can they be sure that their code does what they intend it to do? This paper presents encouraging results in the application of mechanized proof to the domain of quantum programming in the context of the SQIR development. It verifies the correctness of a range of a quantum algorithms including Grover's algorithm and quantum phase estimation, a key component of Shor's algorithm. In doing so, it aims to highlight both the successes and challenges of formal verification in the quantum context and motivate the theorem proving community to target quantum computing as an application domain.
