Cargando…
Certified Quantum Computation in Isabelle/HOL
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...
Autores principales: | , , |
---|---|
Formato: | Online Artículo Texto |
Lenguaje: | English |
Publicado: |
Springer Netherlands
2020
|
Materias: | |
Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC8550268/ https://www.ncbi.nlm.nih.gov/pubmed/34720282 http://dx.doi.org/10.1007/s10817-020-09584-7 |
_version_ | 1784590924324536320 |
---|---|
author | Bordg, Anthony Lachnitt, Hanna He, Yijun |
author_facet | Bordg, Anthony Lachnitt, Hanna He, Yijun |
author_sort | Bordg, Anthony |
collection | PubMed |
description | 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. |
format | Online Article Text |
id | pubmed-8550268 |
institution | National Center for Biotechnology Information |
language | English |
publishDate | 2020 |
publisher | Springer Netherlands |
record_format | MEDLINE/PubMed |
spelling | pubmed-85502682021-10-29 Certified Quantum Computation in Isabelle/HOL Bordg, Anthony Lachnitt, Hanna He, Yijun J Autom Reason Article 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. Springer Netherlands 2020-12-24 2021 /pmc/articles/PMC8550268/ /pubmed/34720282 http://dx.doi.org/10.1007/s10817-020-09584-7 Text en © The Author(s) 2020 https://creativecommons.org/licenses/by/4.0/Open AccessThis article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/ (https://creativecommons.org/licenses/by/4.0/) . |
spellingShingle | Article Bordg, Anthony Lachnitt, Hanna He, Yijun Certified Quantum Computation in Isabelle/HOL |
title | Certified Quantum Computation in Isabelle/HOL |
title_full | Certified Quantum Computation in Isabelle/HOL |
title_fullStr | Certified Quantum Computation in Isabelle/HOL |
title_full_unstemmed | Certified Quantum Computation in Isabelle/HOL |
title_short | Certified Quantum Computation in Isabelle/HOL |
title_sort | certified quantum computation in isabelle/hol |
topic | Article |
url | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC8550268/ https://www.ncbi.nlm.nih.gov/pubmed/34720282 http://dx.doi.org/10.1007/s10817-020-09584-7 |
work_keys_str_mv | AT bordganthony certifiedquantumcomputationinisabellehol AT lachnitthanna certifiedquantumcomputationinisabellehol AT heyijun certifiedquantumcomputationinisabellehol |