TY - JOUR T1 - Verified Optimization in a Quantum Intermediate Representation Y1 - 2019 A1 - Kesha Hietala A1 - Robert Rand A1 - Shih-Han Hung A1 - Xiaodi Wu A1 - Michael Hicks AB -

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.

UR - https://arxiv.org/abs/1904.06319 ER -