A DoD Multidisciplinary University Research Initiative (MURI).


The looming appearance of universal quantum computers makes it is imperative to devise methods for correctly programming such devices. Quantum algorithms are complex, and quantum computers explore alternative computation branches in superposition, so programming mistakes in even minor parts of the code can alter the quantum state and invalidate the final result. Debugging is inappropriate in the quantum setting, since it requires examining the program state, and besides the high cost of early quantum computers will make trial runs prohibitively expensive. The goal of this project is to devise novel methods for ensuring quantum programs are correct. We will use emerging alternative models for quantum computing that we are developing to devise methods to reason effectively about quantum computations, and we test our methods on the functional quantum programming language Quipper.


  • Project Review: On March 8, 2019, we held our third annual project review, this time at the Joint Center for Quantum Information and Computer Science at the University of Maryland.
  • New Team: As we enter the option years of the project, we’re happy to welcome a new team from QuICS, the Joint Center for Quantum Information and Computer Science at the University of Maryland. The members are Andrew Childs, the Co-Director of the Center who’s also an expert on quantum algorithms, and Xioadi Wu, an Assistant Professor of Computer Science and a member of the Center who works on verfication of quantum programs and Hoare logic. Robert Rand now is a postdoc working with the QuICS team.
  • Project Review: On December 15, 2017, we held our second annual project review, again at the Simons Institute in Berkeley.
  • Project Review: On November 29, 2016, we held our first annual project review at the Simons Institute in Berkeley.
  • Kickoff Meeting: On January 25-26, 2016 we held our kickoff meeting at the computer science department of Tulane University.