Certified quantum computation in Isabelle/HOL

DOI10.1007/s10817-020-09584-7OpenAlexW3113530183MaRDI QIDQ2666954

Anthony Bordg, Yijun He, Hanna Lachnitt

Publication date: 23 November 2021

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2012.13925

zbMATH Keywords

quantum computingquantum teleportationDeutsch-Jozsa algorithmIsabelle/HOLcertificationno-cloningDeutsch's algorithmquantum prisoner's dilemma

Mathematics Subject Classification ID

Related Items (1)

A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL

Uses Software

• Isabelle/HOL
• Locales
• Jordan Normal Forms
• Archive Formal Proofs
• Matrix_Tensor

Cites Work

• Locales: a module system for mathematical theories
• Quantum Computation and Quantum Information
• Quantum theory, the Church–Turing principle and the universal quantum computer
• Teleporting an unknown quantum state via dual classical and Einstein-Podolsky-Rosen channels
• Quantum Games and Quantum Strategies
• A single quantum cannot be cloned
• Formal verification of quantum algorithms using quantum Hoare logic
• Unnamed Item
• Unnamed Item

This page was built for publication: Certified quantum computation in Isabelle/HOL