



@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 = {<p>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.</p>},
	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 {2404,
	title = {Verified Optimization in a Quantum Intermediate Representation},
	year = {2019},
	month = {04/12/2019},
	abstract = {<p>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.</p>},
	url = {https://arxiv.org/abs/1904.06319},
	author = {Kesha Hietala and Robert Rand and Shih-Han Hung and Xiaodi Wu and Michael Hicks}
}
