QWIRE Practice: Formal Verification of Quantum Circuits in Coq
  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.
