I am a PhD student in the PLClub at UPenn; I finished my Master’s in the Software Practices Lab at UBC in 2022. My research interests include dependent types, type theory, proof assistants, compilers, and mathematical logic.

Research

My current advisor is Stephanie Weirich. With fellow student Yiyun Liu, we have worked on the Dependent Calculus of Indistinguishability (DCOI), a dependent type system with dependency tracking and which internalizes a notion of indistinguishability as propositional equality. I have also worked on Stratified Type Theory (StraTT), where instead of stratifying type universes into a hierarchy, we stratify entire judgements instead.

In the past, I’ve worked with William J. Bowman on two projects, both of which are about sized types, a type-based method of checking termination of recursive functions. The first, Is Sized Typing for Coq Practical?, explores the viability of an implementation of fully-inferred sized types in Coq’s kernel in terms of performance and metatheory, and has been accepted in the Journal of Functional Programming. The second, Sized Dependent Types in Extensional Type Theory, is my Master’s thesis, and proves the logical consistency of a type theory with explicit, higher-rank, bounded size quantification by compiling it to a type theory whose consistency is more trusted. The work previously placed third in the Student Research Competition entry at POPL 2022 as Towards a Syntatic Model of Sized Dependent Types.