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:

Past publications from members of this project: