论文标题
Isabelle/HOL中的认证量子计算
Certified Quantum Computation in Isabelle/HOL
论文作者
论文摘要
在本文中，我们提出了一种持续的努力，以使用证明助手isabelle/hol形式化量子算法并导致量子信息理论。正式方法对于算法和协议的安全性至关重要，我们预计将来它们可以广泛用于量子计算。我们已经根据量子电路的矩阵表示形式开发了一个大型库来用于伊莎贝尔中的量子计算，成功地正式化了无关定理，量子传送，德意志的算法，德意志 - 乔兹斯萨算法和量子囚犯的困境。我们讨论了在量子游戏理论领域的工作结果做出的设计选择并报告。
In this article we present an ongoing effort to formalise quantum algorithms and results in quantum information theory using the proof assistant Isabelle/HOL. Formal methods being critical for the safety and security of algorithms and protocols, we foresee their widespread use for quantum computing in the future. We have developed a large library for quantum computing in Isabelle based on a matrix representation for quantum circuits, successfully formalising the no-cloning theorem, quantum teleportation, Deutsch's algorithm, the Deutsch-Jozsa algorithm and the quantum Prisoner's Dilemma. We discuss the design choices made and report on an outcome of our work in the field of quantum game theory.
