QWIRE Practice: Formal Verification of Quantum Circuits in Coq

Abstract

We describe an embedding of the QWIRE quantum circuit language in the Coq proof assistant. This allows programmers to write quantum circuits using high-level abstractions and to prove properties of those circuits using Coq's theorem proving features. The implementation uses higher-order abstract syntax to represent variable binding and provides a type-checking algorithm for linear wire types, ensuring that quantum circuits are well-formed. We formalize a denotational semantics that interprets QWIRE circuits as superoperators on density matrices, and prove the correctness of some simple quantum programs.

arXiv commentIn Proceedings QPL 2017, arXiv:1802.09737

References in corpus (2)

• LIQUi|>: A Software Design Architecture and Domain-Specific Language for Quantum Computing
• Formalization of Quantum Protocols using Coq

Cited by in corpus (29)

• Towards Large-scale Functional Verification of Universal Quantum Circuits
• A Verified Optimizer for Quantum Circuits
• A Deductive Verification Framework for Circuit-building Quantum Programs
• ReQWIRE: Reasoning about Reversible Quantum Circuits
• symQV: Automated Symbolic Verification of Quantum Programs
• Certified Quantum Computation in Isabelle/HOL
• A Tool For Debugging Quantum Circuits
• Proving Quantum Programs Correct
• Classical Control, Quantum Circuits and Linear Logic in Enriched Category Theory
• A Survey on Theorem Provers in Formal Methods
• Symbolic Execution for Quantum Error Correction Programs
• Efficient Formal Verification of Quantum Error Correcting Programs
• Linear Dependent Type Theory for Quantum Programming Languages
• On the need for effective tools for debugging quantum programs
• CertiQ: A Mostly-automated Verification of a Realistic Quantum Compiler
• Reasoning about Parallel Quantum Programs
• Symbolic Reasoning about Quantum Circuits in Coq
• Formal Methods for Quantum Programs: A Survey
• Verified Optimization in a Quantum Intermediate Representation
• Quantum Circuit Mutants: Empirical Analysis and Recommendations
• Verifying Quantum Phase Estimation (QPE) using Prove-It
• Automating Equational Proofs in Dirac Notation
• Quantum Hoare Type Theory: Extended Abstract
• Quantum Programming Made Easy
• The Quantum Monadology
• A HoTT Quantum Equational Theory (Extended Version)
• Compositional theories for host-core languages
• Formal Verification of Quantum Ancilla Safety
• Formal Verification of Cyber-Physical Systems using Theorem Proving (Invited Paper)