Certified Quantum Computation in Isabelle/HOL

Abstract

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.

J Autom Reasoning (2020)

References in corpus (5)

• Quantum Games and Quantum Strategies
• The Inductive Approach to Verifying Cryptographic Protocols
• Comment on `Quantum Games and Quantum Strategies'
• QWIRE Practice: Formal Verification of Quantum Circuits in Coq
• Formalization of Quantum Protocols using Coq

Cited by in corpus (7)

• Formal Verification of Quantum Programs: Theory, Tools and Challenges
• Proving Quantum Programs Correct
• Efficient Formal Verification of Quantum Error Correcting Programs
• Quantum Software Engineering Challenges from Developers' Perspective: Mapping Research Challenges to the Proposed Workflow Model
• Formal Methods for Quantum Programs: A Survey
• Automating Equational Proofs in Dirac Notation
• Hybrid Path-Sums for Hybrid Quantum Programs