Verified Optimization in a Quantum Intermediate Representation

Kesha Hietala (University of Maryland), Robert Rand (University of Maryland), Shih-Han Hung (University of Maryland), Xiaodi Wu (University of Maryland), Michael Hicks (University of Maryland)

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.