Title: 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.