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 have developed the
redtt proof assistant
for Cartesian cubical type theory.
Implementing a Modal Dependent Type Theory.
International Conference on Functional Programming (ICFP), 2019.
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