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.