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

Osama M. Raisuddin, Suvranu De

Anthony Bordg, Hanna Lachnitt, Yijun He

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.

M. S. Ramkarthik, Pranay Barkataki

康弘 都倉

Mnacho Echenim, Mehdi Mhalla

We present a formalization in Isabelle/HOL of quantum projective measurements, a class of measurements involving orthogonal projectors that is frequently used in quantum computing. We also formalize the CHSH inequality, a result that holds on arbitrary probability spaces, which can used to disprove the existence of a local hidden-variable theory for quantum mechanics.

Joseph M. Landsberg