### Abstract

This work is an effort to formalise some quantum algorithms and results in quantum information theory. 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.

### License

BSD License

### Topics

- Computer science/Algorithms/Quantum computing
- Mathematics/Physics/Quantum information

### Session Isabelle_Marries_Dirac

- Basics
- Binary_Nat
- Quantum
- Complex_Vectors
- Tensor
- More_Tensor
- Measurement
- Entanglement
- Quantum_Teleportation
- Deutsch
- Deutsch_Jozsa
- No_Cloning
- Quantum_Prisoners_Dilemma

### Depends on

- Matrices, Jordan Normal Forms, and Spectral Radius Theory
- Tensor Product of Matrices
- Vector Spaces

### Used by

- Quantum projective measurements and the CHSH inequality

## Cite

×

Isabelle_Marries_Dirac-AFP

    @article{Isabelle_Marries_Dirac-AFP,
      author  = {Anthony Bordg and Hanna Lachnitt and Yijun He},
      title   = {Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/Isabelle_Marries_Dirac.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Nov 30, 2020 : Isabelle2020