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.

The First International Workshop on Programming Languages for Quantum Computing

Extended abstract accepted for a merged talk at PLanQC 2020 co-located with POPL ‘20.