Verified Optimization in a Quantum Intermediate Representation
Logic in Computer Science
2019-12-09 v4 Emerging Technologies
Programming Languages
Quantum Physics
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 `quantum assembly' 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's use as a tool for general verification by proving several quantum programs correct.
Keywords
Cite
@article{arxiv.1904.06319,
title = {Verified Optimization in a Quantum Intermediate Representation},
author = {Kesha Hietala and Robert Rand and Shih-Han Hung and Xiaodi Wu and Michael Hicks},
journal= {arXiv preprint arXiv:1904.06319},
year = {2019}
}
Comments
Superceded by arXiv:1912.02250