QWIRE Practice: Formal Verification of Quantum Circuits in Coq

Robert Rand
(University of Pennsylvania)
Jennifer Paykin
(University of Pennsylvania)
Steve Zdancewic
(University of Pennsylvania)

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.

In Bob Coecke and Aleks Kissinger: Proceedings 14th International Conference on Quantum Physics and Logic (QPL 2017), Nijmegen, The Netherlands, 3-7 July 2017, Electronic Proceedings in Theoretical Computer Science 266, pp. 119–132.
Published: 27th February 2018.

ArXived at: http://dx.doi.org/10.4204/EPTCS.266.8 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org