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. Check out my new research blog! Access my curriculum vitae
I study the syntax and semantics of type theory and programming languages through the lens of categorical algebra and topos theory, with an aim toward building better interactive proof assistants. I am interested in the design and metatheory of program module calculi as in ML family languages.
My colleagues and I have developed the redtt and cooltt proof assistants for Cartesian cubical type theory.
|Aug. 2020||thesis proposal presented and accepted|
|Jul. 2019||received ICFP '19 Distinguished Paper Award|
|Jun. 2019||received FSCD '19 Best Paper Award for Junior Researchers|
Preprint Syntactic categories for dependent type theory: sketching and adequacy
A Cubical Language for Bishop Sets
To appear Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
Journal of the ACM (accepted pending minor revision)
To appear Normalization for Cubical Type Theory
36th Annual Symposium on Logic in Computer Science.
Higher-Order Functions and Brouwer's Thesis
Journal of Functional Programming, Bob Harper Festschrift Collection.
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.
(Conference talks listed with publications.)
Logical Relations As Types
CCS Colloquium, Augusta University.
Normalization for Cubical Type Theory
Pittsburgh's HoTT Seminar.
Objective Metatheory of (Cubical) Type Theories
redtt and the future of Cartesian cubical type theory.
Every Proof Assistant
Objective Metatheory of Dependent Type Theories.
(Cubical) Computability Structures.
MURI Grant Meeting
Gluing Models of Type Theory Along Flat Functors.
CMU HoTT Seminar.
Cubical Exact Equality and Categorical Gluing.
International Conference on Homotopy Type Theory, 2019.
XTT: Cubical Syntax for Extensional Equality (without equality reflection).
Algebraic Type Theory and the Gluing Construction.
CMU HoTT Seminar.
redtt: implementing cartesian cubical type theory.
Dagstuhl Seminar 18341: Formalization of Mathematics in Type Theory.
Notes A Synthetic Realignment Theorem
|Apr. 2020||Notes An OK Version of Type Theory|
|Feb. 2020||Notes Connectives in Semantics of Type Theory|
Guest lecture for Constructive Logic (15-317) at CMU.
Implementing Inference Rules in Standard ML
Tutorial for Constructive Logic (15-317) as CMU.
|Fall 2018||TA for Constructive Logic (15-317) with Karl Crary.|
|Fall 2017||TA for Constructive Logic (15-317) with Frank Pfenning.|
I have served as an external reviewer or subreviewer for CSL (2021), ESOP (2021), FSCD (2019, 2020), FoSSaCS (2021), LICS (2017, 2021); and as a referee for MSCS.
I am a mentor for the SIGPLAN long-term mentoring program for programming languges researchers (SIGPLAN-M).
|2019||ICFP '19 Distinguished Paper Award|
|2019||FSCD '19 Best Paper Award for Junior Researchers|
|2011||W.K. Pritchett Prize in Elementary Greek, UC Berkeley|