I design and implement programming languages. I aim for language abstractions with rich expressive power, fast implementations, and strong guarantees. I invite broad-minded, technically strong students (PhD and undergraduate) to join me in exploring fun ideas in PL and beyond.
Rocqet makes it easier to build extensible trustworthy systems, like verified compilers, in Rocq.
[ full paper | TR | Rocqet ]
Compiling high-level, modular algebraic effects to low-level, swift stack switching
[ full paper | the Lexa language ]
A compiler factorizes recursive probabilistic programs for scalable inference.
[ full paper | TR ]
Reconciling algebraic data types with scalable extensibility
[ full paper ]
An object-oriented idea lends itself to reusable proofs!
[ full paper | TR | implementation ]
Symbolic methods (a type system and an analysis) aid in neural-network-based inference.
[ full paper | TR ]
Reasoning principles for probabilistic programs that model rational agents
[ full paper | TR | mechanized proof ]
Handlers for “effectful effects”? Yes, with a type system to defend abstractions.
[ full paper | TR | mechanized proof ]
Robots plan paths against both noise and adversarial uncertainty.
[ full paper | code ]
Algebraic effects (and hence exceptions, asynchrony, ...) made modular
[ full paper | TR | mechanized proof ]
A lot of polymorphism and extensibility in a lightweight package
[ full paper | TR ]
The flexibility of unchecked exceptions, the static guarantees of checked exceptions, and good performance too
[ full paper | TR ]
An expressive, lightweight genericity mechanism with better code reuse and stronger static checking
[ full paper | TR ]
Spring 2025
CS 245
Logic and Computation
Winter 2025
CS 747
Formal Reasoning with Proof Assistants
Winter 2025
CS 444/644
Compiler Construction
Spring 2024
CS 842
Probabilistic and Differentiable Languages
Committee Chairs:
The Programming Journal (Vol. 10) Artifact Evaluation
Review Committees: