Certified Quantum Computation in Isabelle/HOL.
Certified Quantum Computation in Isabelle/HOL.
复制标题
DOI：
10.1007/s10817-020-09584-7
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
He Y
中科院分区：
文献类型：
--
作者：
Bordg A;Lachnitt H;He Y
在这篇文章中，我们介绍了一项正在进行的使用证明助手Isabelle/HOL形式化量子算法和量子信息论结果的努力。形式化方法对算法和协议的安全性和安全性至关重要，我们预计它们在未来将在量子计算中广泛使用。我们在Isabelle开发了一个基于量子电路矩阵表示的大型量子计算库，成功地形式化了不可克隆定理、量子隐形传态、Deutsch算法、Deutsch-Jozsa算法和量子囚徒困境。我们讨论了所做的设计选择，并报告了我们在量子博弈论领域的工作结果。
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.
登录
查看更多内容
影响因子：
5.6
作者：
Kammueller, Florian
通讯作者：
Kammueller, Florian
影响因子：
64.8
作者：
WOOTTERS, WK;ZUREK, WH
通讯作者：
ZUREK, WH
影响因子：
8.6
作者：
BENNETT, CH;BRASSARD, G;WOOTTERS, WK
通讯作者：
WOOTTERS, WK
DOI：
10.1098/rspa.1985.0070
发表时间：
1985-01-01
期刊：
PROCEEDINGS OF THE ROYAL SOCIETY OF LONDON SERIES A-MATHEMATICAL PHYSICAL AND ENGINEERING SCIENCES
影响因子：
--
作者：
DEUTSCH, D
通讯作者：
DEUTSCH, D
影响因子：
2.6
作者：
DIEKS, D
通讯作者：
DIEKS, D