I am a Ph.D. student at Programming Languages Group, University of Waterloo (started from Fall 2021). I am co-supervised by Yizhou Zhang and Ondřej Lhoták.
I am generally interested in code-level verification of real-world software and interactive theorem proving (Coq and Agda).
Now I'm actively working with Yizhou on type system based approaches targeting efficient, reliable and certified probabilistic programming.
[DOI]