QWIRE Practice: Formal Verification of Quantum Circuits in Coq

TL;DR

This paper presents a formal verification framework for quantum circuits by embedding the QWIRE language into Coq, enabling high-level circuit design and proof of properties with rigorous semantics.

Contribution

It introduces a Coq embedding of QWIRE with a type-checker for linear types and formal semantics, facilitating verified quantum programming.

Findings

Successfully formalized QWIRE semantics as superoperators

Proved correctness of simple quantum programs

Implemented a type-checking algorithm for well-formed circuits

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.