This is a Coq implementation of the QWIRE quantum programming language, described in the following papers by Jennifer Paykin, Robert Rand, Dong-Ho Lee and Steve Zdancewic:
- QWIRE: a core language for quantum circuits.
- QWIRE Practice: Formal Verification of Quantum Circuits in Coq
- ReQWIRE: Reasoning about Reversible Quantum Circuits
- Phantom Types for Quantum Programs
Rennela and Staton's Classical Control, Quantum Circuits and Linear Logic in Enriched Category Theory provides a categorical semantics for QWIRE.
QWIRE is compatible with Coq versions 8.12 - 8.15.
This project depends on QuantumLib, which you can install with:
opam pin coq-quantumlib https://github.com/inQWIRE/QuantumLib.git
Run make to compile the core (preliminary and implementation) files and make all to compile proofs of QWIRE programs. Run make qasm to compile the files that convert QWIRE to QASM. We recommend using Company Coq with QWIRE in light of its support for unicode.
Preliminaries
- Monad.v : An implementation of some basic monads
- Monoid.v : A typeclass and solver for commutative monoids, modified from LinearTypingContexts
Implementation of QWIRE
- Contexts.v : Defines wire types and typing contexts
- HOASCircuits.v : Defines QWIRE circuits using higher-order abstract syntax
- DBCircuits.v : Compiling HOAS to De Bruijin style circuits
- TypeChecking.v : Circuit notations and tactics for proving well-typedness
- Denotation.v : Defines the denotational semantics of QWIRE circuits and proves its (quantum mechanical) validity
- HOASLib.v : A library of basic circuits used in QWIRE programming
- SemanticLib.v : Proves the semantic properties of HOASLib circuits
- HOASExamples.v : Additional examples of HOAS circuits
- Composition.v : States and admits compositionality lemmas (used in the following five files)
- Ancilla.v : Defines the correctness of circuits using ancilla assertions
- Symmetric.v : Syntactic conditions for guaranteeing the validity of assertions
- Oracles.v : Compilation of boolean expressions to QWIRE circuits
Verification of QWIRE circuits
- Arithmetic.v : Verification of a quantum adder
- Deutsch.v : Variants on Deutsch's Algorithm
- Equations.v : Equalities on small circuits
- HOASProofs.v : Additional proofs, including coin flips and teleportation
Compilation to QASM (i.e., OpenQASM 2.0)
- QASM.v : Compilation from QWIRE to QASM
- QASMPrinter.v : A printer for compiled circuits, for execution on a quantum computer/simulator
- QASMExamples.v : Examples of circuit compilation
The QWIRE project has benefited from the support of the Air Force Office of Scientific Research under the MURI grant number FA9550-16-1-0082 entitled, “Semantics, Formal Reasoning, and Tool Support for Quantum Programming” and the U.S. Department of Energy, Office of Science, Office of Advanced Scientific Computing Research, Quantum Testbed Pathfinder Program under Award Number DE-SC0019040.