A Verified Optimizer for Quantum Circuits. Kesha Hietala, Robert Rand, Liyi Li, Shih-Han Hung, Xiaodi Wu, and Michael Hicks. ACM Transactions on Programming Languages and Systems (TOPLAS), 45(3), September 2023. Extends POPL'21 paper.

We present VOQC, the first fully verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called SQIR, a small quantum intermediate representation, 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 programs denote complex-valued matrices, as is standard in quantum computation, but we treat matrices symbolically in order to reason about programs that use an arbitrary number of quantum bits. SQIR's careful design and our provided automation make it possible to write and verify a broad range of optimizations in VOQC, including full-circuit transformations from cutting-edge optimizers.

[ .pdf ]

@article{hietala22voqc-journal,
  author = {Kesha Hietala and Robert Rand and Liyi Li and Shih-Han Hung and Xiaodi Wu and Michael Hicks},
  title = {A Verified Optimizer for Quantum Circuits},
  journal = {{ACM} Transactions on Programming Languages and Systems (TOPLAS)},
  month = sep,
  volume = 45,
  number = 3,
  note = {Extends POPL'21 paper},
  year = {2023}
}

This file was generated by bibtex2html 1.99.