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: | Bordg, Anthony, Lachnitt, Hanna, He, Yijun |
---|---|
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 |
Ejemplares similares
-
Algebraically Closed Fields in Isabelle/HOL
por: de Vilhena, Paulo Emílio, et al.
Publicado: (2020) -
A Verified Implementation of Algebraic Numbers in Isabelle/HOL
por: Joosten, Sebastiaan J. C., et al.
Publicado: (2018) -
Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL
por: Guttmann, Walter
Publicado: (2020) -
Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL
por: Bottesch, Ralph, et al.
Publicado: (2020) -
Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL
por: Thiemann, René, et al.
Publicado: (2020)