Jon Sterling

9225 Gates Hillman Center
School of Computer Science
Carnegie Mellon University
5000 Forbes Ave
Pittsburgh, PA 15213

ORCID iD icon

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.

Recent News

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

Recent Drafts

Oct. 2020 Draft Note A Synthetic Realignment Theorem
Jul. 2020
Draft paper Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
J. Sterling, R. Harper.
Coming soon Higher-Order 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
J. Sterling, C. Angiuli, and D. Gratzer.
Draft Note Connectives in Semantics of Type Theory


ICFP '19 Implementing a Modal Dependent Type Theory.
D. Gratzer, J. Sterling, and L. Birkedal.
International Conference on Functional Programming (ICFP), 2019.
Distinguished Paper Award.
FSCD '19 Cubical Syntax for Reflection-Free Extensional Equality.
J. Sterling, C. Angiuli, and D. Gratzer.
International Conference on Formal Structures for Computation and Deduction (FSCD), 2019.
Best Paper Award For Junior Researchers.
LFMTP '18 The RedPRL Proof Assistant.
C. Angiuli, E. Cavallo, K. Hou (Favonia), R. Harper, and J. Sterling.
International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), 2018.
Invited Paper
LICS '18 Guarded Computational Type Theory.
J. Sterling, R. Harper.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18).
Apr. 2016 Dependent Types for Pragmatics.
D. McAdams, J. Sterling.
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.

Selected Talks

(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.
Mar. 2020 (Cubical) Computability Structures.
MURI Grant Meeting
Jan. 2020 Gluing Models of Type Theory Along Flat Functors.
J. Sterling and C. Angiuli
CMU HoTT Seminar.
HoTT '19 Cubical Exact Equality and Categorical Gluing.
J. Sterling, C. Angiuli, and D. Gratzer.
International Conference on Homotopy Type Theory, 2019.
TYPES '19 XTT: Cubical Syntax for Extensional Equality (without equality reflection).
J. Sterling, C. Angiuli, and D. Gratzer.
TYPES, 2019.
Apr. 2019 Algebraic Type Theory and the Gluing Construction.
CMU HoTT Seminar.
Aug. 2018 redtt: implementing cartesian cubical type theory.
C. Angiuli, E. Cavallo, Favonia, R. Harper, A. Mőrtberg, and J. Sterling.
Dagstuhl Seminar 18341: Formalization of Mathematics in Type Theory.

Selected Lectures

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.

Academic Service

I have served as an external reviewer or subreviewer for LICS (2017), FSCD (2019, 2020), CSL (2021); and as a referee for MSCS.

Awards and Honors

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

Other Activities

Together with my co-hosts David Christiansen and Darin Morrison, I helped create The Type Theory Podcast.