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. 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 
Jun. 2021 
Abstract
A metalanguage for multiphase modularity

Dec. 2020 
Preprint
Syntactic categories for dependent type theory: sketching and adequacy

Feb. 2020 
Preprint
A Cubical Language for Bishop Sets
arXiv preprint
latest version
(revised May 2021)

JACM 
To appear
Logical Relations as Types: ProofRelevant Parametricity for Program Modules
Journal of the ACM (accepted pending minor revision)
arXiv preprint,
latest version
(revised May 2021)

LICS '21 
To appear
Normalization for Cubical Type Theory
36th Annual Symposium on Logic in Computer Science

JFP 
Higher order functions and Brouwer's Thesis
Journal of Functional Programming, Bob Harper Festschrift Collection 
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 RedPRL Proof Assistant
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.)
May 2021 
Normalization for Cubical Type Theory
Padova Logic Seminar 
Apr. 2021 
Logical Relations As Types
CCS Colloquium, Augusta University. 
Feb. 2021 
Normalization for Cubical Type Theory
Pittsburgh's HoTT Seminar 
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 
Oct. 2020 
Notes
A Synthetic Realignment Theorem

Apr. 2020  Notes An OK Version of Type Theory 
Feb. 2020  Notes Connectives in Semantics of Type Theory 
Fall 2017 
Lecture
Substructural Deduction
Guest lecture for Constructive Logic (15317) at CMU 
Fall 2017 
Lecture
Implementing Inference Rules in Standard ML
Tutorial for Constructive Logic (15317) as CMU 
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 CSL (2021), ESOP (2021), FSCD (2019, 2020), FoSSaCS (2021), LICS (2017, 2021); and as a referee for LMCS and MSCS.
I am a mentor for the SIGPLAN longterm mentoring program for programming languges researchers (SIGPLANM).
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 