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.
- 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.