I am a PhD student in the PLClub at UPenn, advised by Stephanie Weirich. Before that, I was a Master’s student in the Software Practices Lab at UBC, advised by William J. Bowman. My research interests include dependent types, type theory, proof assistants, and compilers.

Here is some of my recent work (details and more can be found in my CV linked in the sidebar):

• Commuting Conversions and Join Points for CBPV will appear at OOPSLA 2026. This work began as a REPL summer project with Madi Gudin and Annabel Levy, supervised by Stephanie Weirich, defining a commuting conversion normalization algorithm for CBPV and proving that it preserves program semantics.

• Consistency of a Dependent Calculus of Indistinguishability (DCOI), work with first author Yiyun Liu and Stephanie Weirich, appeared at POPL 2025 in Denver, Colorado. This is followup work on DCOI where we prove a variant DCOIω with a universe hierarchy to be consistent and normalizing.

  DCOI was introduced in our (along with Jessica Shi) POPL 2024 paper Internalizing Indistiguishability with Dependent Types, which is a dependent type system with dependency tracking, a notion of indistinguishability with respect to dependency levels, and the internalization of indistinguishability as propositional equality.

• I presented work with Stephanie Weirich on Stratified Type Theory (StraTT) at ESOP 2025 in Hamilton, Ontario. This is a type theory where instead of stratifying type universes into a hierarchy, we stratify entire judgements themselves.
• At ICFP 2023, I presented work with Yufeng Li and William J. Bowman, Is Sized Typing for Coq Practical?, which was published at JFP in 2023. This work explores the viability of an implementation of fully inferred sized types in Coq’s kernel in terms of performance and metatheory.

Outside of research, I enjoy drinking funky aeropress coffees, taking film photos with my point-and-shoot, reading sci-fi novels, and watching queer films.

---