My main interest is in applying techniques from programming languages and formal verification to the domain of quantum computation. Two of my main projects are the QWIRE quantum circuit language (with Jennifer Paykin) and the VOQC verified optimizing compiler (with Kesha Hietala). I’m currently interested in verified optimization, error-correction, type systems and programming abstractions for quantum computing.
I’m working on a book on verified quantum programming! Email me if you’d like to use the book for your own course.
If you’re interested in doing research with me: Please reach out!
May 2023 The journal version of A Verified Optimizer for Quantum Circuits was accepted to TOPLAS!
April 2023 Our paper A Formally Certified End-to-End Implementation of Shor’s Factorization Algorithm was accepted to the Proceedings of the National Academy of Sciences (PNAS)!
December 2022 I received an AFOSR Young Investigator Research Program award to conduct research on Formally Verifying Graphical Quantum Calculi!