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, compilers, and mathematical logic.

Here is some of my recent work:

• 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 will be presenting 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.

Details and more can be found in my CV linked in the sidebar.

Outside of research, I enjoy drinking funky aeropress coffees, taking photos with my film point-and-shoot, knitting and crocheting more scarves and hats than I need, reading sci-fi novels, and watching open-captioned movies.