Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Isabelle Marries Dirac: a Libr...

view this post on Zulip Email Gateway (Nov 30 2020 at 09:09):

From: "Thiemann, René" <>
Dear all,

I’m happy to announce a new entry in the AFP on quantum computation and quantum information.

Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information
by Anthony Bordg, Hanna Lachnitt and Yijun He

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


Last updated: Jul 15 2022 at 23:21 UTC