I am a doctoral student of Robert Harper at Carnegie Mellon University studying type theory, programming languages and semantics. Previously I received a B.A. in Linguistics from U.C. Berkeley. My other interests include category theory, topos theory, formalization of mathematics, Assyriology, and ancient languages and literature.
I study the syntax and semantics of type theory and programming languages, through an algebraic lens. I am particularly interested in the semantics of syntax, applying categorical techniques such as gluing to obtain abstract normalization results. My colleagues and I are developing the redtt proof assistant for Cartesian cubical type theory.
Some of my collaborators include Carlo Angiuli, Lars Birkedal, Evan Cavallo, David Thrane Christiansen, Favonia, Daniel Gratzer, Robert Harper, Darin Morrison, and Anders Mörtberg.