For quantum computers to be useful, we need to provide software development tools for would-be quantum programmers. Our main project is the VOQC compiler, the first fully verified compiler for quantum programs. It takes programs written in a small quantum intermediate representation, SQIR, and both maps them to a specified architecture and aggressively optimizes them to use a minimal number of quantum gates. We also use SQIR to directly verify quantum programs, such as Quantum Phase Estimation or Deutsch-Jozsa, which we can then convert to IBM’s OpenQASM standard and execute on real world devices.

Other activities include:

• A logic for analyzing the robustness of quantum programs.
• Developing the QWIRE quantum programming language.
• Reasoning about errors in quantum programs.
• Rich types for quantum programs.
• An introduction to quantum computing in the Coq proof assistant.

Past publications from members of this project:

• Gottesman Types for Quantum Programs, QPL 2020 (to appear). Robert Rand, Aarthi Sundaram, Kartik Singhal, and Brad Lackey.
• A Verified Optimizer for Quantum Circuits, draft April 2020. Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, Michael Hicks. Mike spoke about this work at the UMass Systems Lunch (video)
• Tracking Errors through Types in Quantum Programs, PLanQC 2020. Kesha Hietala, Robert Rand, Michael Hicks.
• Verified translation between low-level quantum languages, PLanQC 2020. Kartik Singhal, Robert Rand, Michael Hicks.
• Verified Optimization in a Quantum Intermediate Representation, QPL 2019 (superceded by “A Verified Optimizer for Quantum Circuits”). Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, Michael Hicks.
• Formal Verification vs. Quantum Uncertainty, SNAPL 2019. Robert Rand, Kesha Hietala, Michael Hicks.
• Quantitative Robustness Analysis of Quantum Programs, POPL 2019. Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks, and Xiaodi Wu.