POPL 2020 (series) / PLanQC 2020 (series) / Programming Languages for Quantum Computing /
Verified translation between low-level quantum languages
We describe the ongoing development of a verified translator between OpenQASM (Open Quantum Assembly Language) and sQIR, a Small Quantum Intermediate Representation used for circuit optimization. Verified translation from and to OpenQASM will allow verified optimization of circuits written in a variety of tools and executed on real quantum computers. This translator is a step toward a verified compilation stack for quantum computing.
This is a merged talk with A Verified Optimizer for Quantum Circuits.