9225 Gates Hillman Center
School of Computer Science
Carnegie Mellon University
5000 Forbes Ave
Pittsburgh, PA 15213
j...@cs.cmu.edu
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 the lens of categorical algebra, 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 |
Jul. 2020 |
Higher-Order Functions and Brouwer's Thesis
(In preparation) |
Jul. 2020 |
Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
. (Draft paper) |
Feb. 2020 |
A Cubical Language for Bishop Sets
. (Draft paper) |
ICFP '19 |
Implementing a Modal Dependent Type Theory.
. International Conference on Functional Programming (ICFP), 2019. Distinguished Paper Award. |
FSCD '19 |
Cubical Syntax for Reflection-Free Extensional Equality.
. International Conference on Formal Structures for Computation and Deduction (FSCD), 2019. Best Paper Award For Junior Researchers. |
LFMTP '18 |
The . International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), 2018. Invited Paper |
LICS '18 |
Guarded Computational Type Theory.
. Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18). |
Apr. 2016 |
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. |
Apr. 2020 |
An OK Version of Type Theory
. (Expository note) |
Feb. 2020 |
Connectives in Semantics of Type Theory
. (Expository note) |
(Conference talks listed with publications.)
Aug. 2020 |
Objective Metatheory of (Cubical) Type Theories
Thesis Proposal |
Jun. 2020 |
redtt and the future of Cartesian cubical type theory.
Every Proof Assistant |
Mar. 2020 |
Objective Metatheory of Dependent Type Theories.
HoTTEST |
Mar. 2020 |
(Cubical) Computability Structures.
MURI Grant Meeting |
Jan. 2020 |
Gluing Models of Type Theory Along Flat Functors.
CMU HoTT Seminar. |
HoTT '19 |
Cubical Exact Equality and Categorical Gluing.
. International Conference on Homotopy Type Theory, 2019. |
TYPES '19 |
XTT: Cubical Syntax for Extensional Equality (without equality reflection).
. TYPES, 2019. |
Apr. 2019 |
Algebraic Type Theory and the Gluing Construction.
CMU HoTT Seminar. |
Aug. 2018 |
redtt: implementing cartesian cubical type theory.
. Dagstuhl Seminar 18341: Formalization of Mathematics in Type Theory. |
Fall 2017 |
Substructural Deduction.
Guest lecture for Constructive Logic (15-317). |
Fall 2017 |
Implementing Inference Rules in Standard ML.
Tutorial for Constructive Logic (15-317), Fall 2017. |
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 for LICS (2017), FSCD (2019, 2020), CSL (2021); and as a referee for MSCS.
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 |