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
David Thrane Christiansen,
Darin Morrison, and
Cubical Syntax for Reflection-Free Extensional Equality
International Conference on Formal Structures for Computation and Deduction (FSCD), 2019
The RedPRL Proof Assistant
International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), 2018
Guarded Computational Type Theory
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18)
Dependent Types for Pragmatics
Redmond J., Pombo Martins O., Nepomuceno Fernández Á. (eds) Epistemology, Knowledge and the Impact of Interaction. Logic, Epistemology, and the Unity of Science, vol 38. Springer, Cham.
Awards and Honors
(2011) W.K. Pritchett Prize in Elementary Greek, UC Berkeley.
Together with my co-hosts David Christiansen and Darin Morrison, I helped
create The Type Theory