Skip to content

Latest commit

 

History

History
69 lines (52 loc) · 3.53 KB

README.md

File metadata and controls

69 lines (52 loc) · 3.53 KB

QWIRE

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:

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 8.5 - 8.8.

This version of the project has no dependencies. Run make to compile the core (preliminary and implementation) files and make all to compile the whole project. We recommend using Company Coq with QWIRE in light of its support for unicode.

Files in this repository

Preliminaries

  • Monad.v : An implementation of some basic monads
  • Monoid.v : A typeclass and solver for commutative monoids, modified from LinearTypingContexts
  • Prelim.v : A variety of general purpose definitions and tactics

Underlying mathematical libraries

  • Complex.v : Complex number library, modified from Coquelicot
  • Matrix.v : Matrix library
  • Quantum.v : Defines unitary matrices and quantum operations

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

  • 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.