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.
I design probabilistic programming languages and implement compilers for sound and scalable inference. My work applies type systems, program analyses, and logical relations to achieve efficient, reliable, and certified probabilistic programming. [CV]
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 continuation-passing style (CPS) compilation and information-flow typing (with a denotational, logical-relations model).
[DOI]
CS 450/650 Computer Architecture
CS 444/644 Compiler Construction
CS 245 & CS 245E Logic and Computation
CS 241 Foundations of Sequential Programs