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 that compiles functional programming–style probabilistic programs into probability-generating functions, a compact and exact compilation target representing measures.
Mappl: A compiler that enables scalable inference by factorizing recursive probabilistic programs via information-flow typing.
[DOI]