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 ].
An object-oriented idea leads to a functional language design for engineering extensible proofs.
Symbolic methods (a type system and an analysis) aid in neural-network-based inference.
Reasoning principles for probabilistic programs that express rational agents
Handlers for “effectful effects”? Yes, with a type system to defend abstractions.
Robots plan paths against both noise and adversarial uncertainty.
Algebraic effects (and hence exceptions, asynchrony, ...) made modular
A lot of polymorphism and extensibility in a lightweight package
The flexibility of unchecked exceptions, the static guarantees of checked exceptions, and good performance too
An expressive, lightweight genericity mechanism with better code reuse and stronger static checking