  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.
