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 (undergrad & grad) to join me in exploring fun ideas in PL and at the intersection of PL with other areas.
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 ]
Winter 2025
CS 444/644 Compiler Construction
Spring 2024
CS 842 Probabilistic and Differentiable Languages
Winter 2024
CS 444/644 Compiler Construction
Spring 2023
CS 245 Logic and Computation