I design and implement programming languages. I aim for language abstractions with rich expressive power, strong guarantees, and efficient implementations. I welcome broad-minded, technically strong students to work with me on fun ideas about programming languages [ URA, URF | MMath, PhD | Postdoc ].
Winter 2024
CS 444/644 Compiler Construction
Spring 2023
CS 245 Logic and Computation
An object-oriented idea leads to a functional language design for engineering extensible 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 express 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 ]