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.
July 2019: Implementing a Modal Dependent Type Theory receives ICFP 2019 Distinguished Paper Award.
June 2019: Cubical Syntax for Reflection-Free Extensional Equality receives FSCD 2019 Best Paper Award for Junior Researchers.
June 2019: Implementing a Modal Dependent Type Theory accepted at ICFP 2019.
April 2019: Cubical Syntax for Reflection-Free Extensional Equality accepted at FSCD 2019.
Implementing a Modal Dependent Type Theory.
International Conference on Functional Programming (ICFP), 2019.
Distinguished Paper Award.
Cubical Syntax for Reflection-Free Extensional Equality.
International Conference on Formal Structures for Computation and Deduction (FSCD), 2019.
Best Paper Award For Junior Researchers.
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
(2019) ICFP 2019 Distinguished Paper Award
(2019) FSCD 2019 Best Paper Award for Junior Researchers
(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