We present voqc, the first verified compiler for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called sqir, which is deeply embedded in Coq. Optimizations and other transformations are expressed as Coq functions, which are proved correct with respect to a semantics of sqir programs. sqir is also sufficiently expressive write source programs and prove them correct. We evaluate voqc's verified optimizations on a series of benchmarks, and it performs comparably to industrial strength compilers. voqc's optimizations reduce total gate counts on average by 8.4% (and rotation gates on average by 16.1%) on a benchmark of 29 circuit programs compared to a 4.7% reduction (resp, a 8.3% reduction) when using IBMâ€™s Qiskit compiler at optimization level 2.

[ .pdf ]

@MISC{hietala19voqc, AUTHOR = {Kesha Hietala and Robert Rand and Shih-Han Hung and Xiaodi Wu and Michael Hicks}, TITLE = {A Verified Optimizer for Quantum Circuits}, MONTH = JUL, YEAR = {2019}, SUBMITTED = {yes} }