Electronic Proceedings in Theoretical Computer Science (Feb 2018)

QWIRE Practice: Formal Verification of Quantum Circuits in Coq

  • Robert Rand,
  • Jennifer Paykin,
  • Steve Zdancewic

DOI
https://doi.org/10.4204/EPTCS.266.8
Journal volume & issue
Vol. 266, no. Proc. QPL 2017
pp. 119 – 132

Abstract

Read online

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.