@article {2491, title = {A Verified Optimizer for Quantum Circuits}, journal = {Proceedings of the ACM on Programming Languages}, volume = {5}, year = {2021}, month = {11/12/2020}, abstract = {

We present VOQC, the first fully 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. We evaluate VOQC\&$\#$39;s verified optimizations on a series of benchmarks, and it performs comparably to industrial-strength compilers. VOQC\&$\#$39;s optimizations reduce total gate counts on average by 17.7\% on a benchmark of 29 circuit programs compared to a 10.7\% reduction when using IBM\&$\#$39;s Qiskit compiler.

}, doi = {https://doi.org/10.1145/3434318}, url = {https://arxiv.org/abs/1912.02250}, author = {Kesha Hietala and Robert Rand and Shih-Han Hung and Xiaodi Wu and Michael Hicks} } @article {2384, title = {Verification Logics for Quantum Programs}, year = {2019}, type = {Originally submitted in March 2016 as a qualifying examination (WPE-II) for the PhD program at the University of Pennsylvania}, abstract = {

We survey the landscape of Hoare logics for quantum programs. We review three papers: \"Reasoning about imperative quantum programs\" by Chadha, Mateus and Sernadas; \"A logic for formal verification of quantum programs\" by Yoshihiko Kakutani; and \"Floyd-hoare logic for quantum programs\" by Mingsheng Ying. We compare the mathematical foundations of the logics, their underlying languages, and the expressivity of their assertions. We also use the languages to verify the Deutsch-Jozsa Algorithm, and discuss their relative usability in practice.

}, url = {https://arxiv.org/abs/1904.04304}, author = {Robert Rand} } @article {2404, title = {Verified Optimization in a Quantum Intermediate Representation}, year = {2019}, month = {04/12/2019}, abstract = {

We present sqire, a low-level language for quantum computing and verification. sqire uses a global register of quantum bits, allowing easy compilation to and from existing {\textquoteleft}quantum assembly\&$\#$39; languages and simplifying the verification process. We demonstrate the power of sqire as an intermediate representation of quantum programs by verifying a number of useful optimizations, and we demonstrate sqire\&$\#$39;s use as a tool for general verification by proving several quantum programs correct.

}, url = {https://arxiv.org/abs/1904.06319}, author = {Kesha Hietala and Robert Rand and Shih-Han Hung and Xiaodi Wu and Michael Hicks} }