Today’s quantum computers can reasonably be described as science experiments: They explore the power of different approaches to harnessing quantum mechanics and show that they can solve contrived problems more efficiently than existing computers. But quantum computers are getting more powerful, achieving milestones in error correction that will allow them to scale and bring practical applications within sight. And yet, we still program them using quantum circuits, a generalization of logic gates to the quantum setting. This is analogous to programming with Boolean circuits, ignoring decades of programming languages advances.

In this talk, I’ll address how programming languages research can make quantum computers useful in practice. What should type systems look like for quantum programs and how should we be testing our programs? What can formal verification bring to the table? And, most importantly, what abstractions can we bring to quantum computing, allowing programmers to translate their ideas into executable code?

We don’t have definitive answers to these questions, in part because programming languages need programmers and mature hardware. Instead, this talk will survey the landscape of quantum programming languages research and explore which ideas from programming languages theory can meaningfully advance quantum computation.

I am an Assistant Professor of Computer Science at the University of Chicago, part of the Programming Languages Research Group and the Chicago Quantum Exchange. I lead the Chicago Quantum Programming Languages Laboratory (ChiQP).

My main interest is in applying techniques from programming languages and formal verification to the domain of quantum computation. Some of my major projects include the QWIRE quantum circuit language, the VOQC verified optimizing compiler, the high-level quantum programming language Qunity, and the BellKAT quantum network specification language. I’m currently interested in verified optimization, error-correction, type systems, and programming abstractions for quantum computing.