|
Isabelle
Marries
Dirac:
a
Library
for
Quantum
Computation
and
Quantum
Information
Title: |
Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information |
Authors:
|
Anthony Bordg (apdb3 /at/ cam /dot/ ac /dot/ uk),
Hanna Lachnitt (lachnitt /at/ stanford /dot/ edu) and
Yijun He (yh403 /at/ cam /dot/ ac /dot/ uk)
|
Submission date: |
2020-11-22 |
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. |
BibTeX: |
@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 = nov,
year = 2020,
note = {\url{https://isa-afp.org/entries/Isabelle_Marries_Dirac.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Depends on: |
Jordan_Normal_Form, Matrix_Tensor, VectorSpace |
Used by: |
Projective_Measurements |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|