Certified Quantum Computation in Isabelle/HOL

被引：13

作者：

Bordg, Anthony ^{[1
]}

Lachnitt, Hanna ^{[2
]}

He, Yijun ^{[3
]}

机构：

[1] Univ Cambridge, Dept Comp Sci & Technol, Cambridge, England

[2] Stanford Univ, Dept Comp Sci, Stanford, CA 94305 USA

[3] Univ Cambridge, Cambridge, England

来源：

JOURNAL OF AUTOMATED REASONING | 2021年 / 65卷 / 05期

基金：

欧洲研究理事会;

关键词：

Isabelle; HOL; Certification; Quantum computing; No-cloning; Quantum teleportation; Deutsch’ s algorithm; Deutsch– Jozsa algorithm; Quantum prisoner’ s dilemma;

D O I：

10.1007/s10817-020-09584-7

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

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.

引用

页码：691 / 709

页数：19

共 18 条

[1] Locales: A Module System for Mathematical Theories [J].