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 
Oct. 2020 
Draft Note
A Synthetic Realignment Theorem

Jul. 2020 
Draft paper
Logical Relations as Types: ProofRelevant Parametricity for Program Modules

Coming soon
HigherOrder Functions and Brouwer's Thesis


Apr. 2020  Draft Note An OK Version of Type Theory 
Feb. 2020 
Draft paper
A Cubical Language for Bishop Sets
. 
Draft Note Connectives in Semantics of Type Theory 
ICFP '19 
Implementing a Modal Dependent Type Theory.
. International Conference on Functional Programming (ICFP), 2019. Distinguished Paper Award. 
FSCD '19 
Cubical Syntax for ReflectionFree 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 MetaLanguages: 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. 
(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 (15317). 
Fall 2017 
Implementing Inference Rules in Standard ML.
Tutorial for Constructive Logic (15317), Fall 2017. 
Fall 2018  TA for Constructive Logic (15317) with Karl Crary. 
Fall 2017  TA for Constructive Logic (15317) with Frank Pfenning. 
I have served as an external reviewer or subreviewer 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 