Verified Optimization in a Quantum Intermediate Representation

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.

Superceded by arXiv:1912.02250

References in corpus (10)

• Quantum Computing in the NISQ era and beyond
• Resource-Aware Quantum Programming with General Recursion and Quantum Control
• Polynomial-time T-depth Optimization of Clifford+T circuits via Matroid Partitioning
• Concrete Categorical Model of a Quantum Circuit Description Language with Measurement
• Synthesis of Quantum Circuits for Linear Nearest Neighbor Architectures
• QWIRE Practice: Formal Verification of Quantum Circuits in Coq
• Verified compilation of space-efficient reversible circuits
• ReQWIRE: Reasoning about Reversible Quantum Circuits
• Optimising Clifford Circuits with Quantomatic
• Next Steps in Quantum Computing: Computer Science's Role

Cited by in corpus (4)

• Quantum Software Engineering: Landscapes and Horizons
• Symbolic Reasoning about Quantum Circuits in Coq
• CertiQ: A Mostly-automated Verification of a Realistic Quantum Compiler
• Quantum Image Processing: the truth, the whole truth, and nothing but the truth about its problems on internal image representation and outcomes recovering