I am a Ph.D. student in the Programming Languages Group at the University of Waterloo (since Fall 2021), co-supervised by Yizhou Zhang and Ondřej Lhoták.
I have a general interest in code-level verification of real-world software and interactive theorem proving, such as Coq, Agda, and Lean.
Currently, I am working with Yizhou on type system–based approaches for efficient, reliable, and certified probabilistic programming.
Geni: A compiler uses generating functions to compactly and exactly represent probabilistic programs.
Mappl: A compiler factorizes recursive probabilistic programs for scalable inference.
[DOI]