Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information

Anthony Bordg 🌐, Hanna Lachnitt 📧 and Yijun He 📧

November 22, 2020

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session Isabelle_Marries_Dirac