Biography
I am an Assistant Professor of Computer Science, part of the Programming Languages Research Group and the Chicago Quantum Exchange.
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!
Recent News
May 2026 Ben Caldwell successfully defended their thesis! Congratulations, Dr. Caldwell!!!
January 2026 VyZX: Formal Verification of a Graphical Quantum Language was accepted to TOPLAS! We will also be presenting VyZX at PLDI 2026!
January 2026 Youngchan Cho presented Efficiently Verifying Quantum Programs with Few T Gates at VMCAI 2026!
Courses
- Topics: Lean and Quantum Computing, Spring 2026
- Topics: Program Logics, Spring 2025
- Topics: Fully Automated Luxury Theorem Proving, Winter 2024
- Programming Languages, University of Chicago, Spring 2023, 2024, Fall 2025
- Picturing Quantum Process, University of Chicago, Fall 2022
- Topics: Advanced Proof Automation, University of Chicago, Spring 2022
- Topics: Quantum Programming and Verification, University of Chicago, Spring 2021
- Programming Proofs, University of Chicago, Winter 2021, 2022, Fall 2023, Winter 2025, 2026,
- Discrete Mathematics, University of Chicago, Fall 2020, 2021, Winter 2023
- Program Analysis and Understanding, University of Maryland, Spring 2019
- Python Programming, University of Pennsylvania, Fall 2015 and Spring 2016