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, type checkers, compilers, and mathematical logic.
Research
My current advisor is Stephanie Weirich. We are exploring a new dependent type theory where instead of stratifying type universes into a hierarchy, we stratify entire judgements instead, and are trying to pin down its consistency and expressivity. I have also worked with other PLClub students on DCOI, a dependent type system with dependency tracking and which internalizes a notion of indistinguishability as propositional equality.
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.
Experience
I most recently was a graduate TA at UPenn for CIS 552 (Advanced Programming), a course on functional programming in Haskell. I have been a graduate TA for two courses at UBC: CPSC 311 (Definition of Programing Languages) in 2020WT1 and 2021WT1, where students learn about various features of PLs and write interpreters for them, and CPSC 312 (Functional and Logic Programming) in 2020WT2, where students get some hands-on experience using Haskell and Prolog. I have also been a student volunteer for POPL 2024, ICFP 2023, POPL 2021, ICFP 2020, and POPL 2020, as well as an attendee at OPLSS 2022 and PLISS 2019.
