Q\textsc{wire} practice: formal verification of quantum circuits in Coq

MaRDI QIDQ3384929zbMATH OpenFDO

Authors

Publication date 17 December 2021

Full work available at URL https://arxiv.org/abs/1803.00699, http://eptcs.web.cse.unsw.edu.au/paper.cgi?QPL2017.8

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Logical foundations of quantum mechanics; quantum logic (quantum-theoretic aspects) (81P10) Quantum computation (81P68)

Recommendations

• QWIRE: a core language for quantum circuits
• Formalization of metatheory of the Quipper quantum programming language in a linear logic
• Towards quantum programs verification: from Quipper circuits to QPMC
• A categorical model for a quantum circuit description language (extended abstract)
• A logic for formal verification of quantum programs

Cites work

• Algebraic effects, linearity, and quantum programming languages
• Classical control, quantum circuits and linear logic in enriched category theory
• Coquelicot: a user-friendly library of real analysis for Coq
• Formalization \textit{of} quantum protocols using Coq
• scientific article; zbMATH DE number 5708038 (Why is no real title available?)
• Invariants of quantum programs: characterisations and generation
• Quantum computation and quantum information. 10th anniversary edition
• Quantum weakest preconditions
• QWIRE: a core language for quantum circuits
• Verified compilation of space-efficient reversible circuits

Cited in

(11)

• Formalization of metatheory of the Quipper quantum programming language in a linear logic
• Formal meta-level analysis framework for quantum programming languages
• A modeling and verification framework for optical quantum circuits
• Certified quantum computation in Isabelle/HOL
• \textit{Re}\(\mathcal{Q}\)\textsc{wire}: reasoning about reversible quantum circuits
• Quantum programming made easy
• QWIRE: a core language for quantum circuits
• \textsf{symQV}: automated symbolic verification of quantum programs
• A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL
• Quantum Hoare type theory: extended abstract
• The quantum monadology

Describes a project that uses

Uses Software

• Coq

This page was built for publication: \(\mathcal{Q}\)\textsc{wire} practice: formal verification of quantum circuits in Coq

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3384929)