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. 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.

Recent News

Jun. 2021 accepted postdoctoral position working with Lars Birkedal
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

Upcoming Presentations

Aug. 26
A metalanguage for multi-phase modularity
J. Sterling, R. Harper
Aug. 30
Normalization for cubical type theory
J. Sterling, C. Angiuli

Recent Drafts

Jul. 2021
Preprint A cost-aware logical framework
Y. Niu, J. Sterling, H. Grodin, and R. Harper
Dec. 2020
Preprint Syntactic categories for dependent type theory: sketching and adequacy
D. Gratzer, J. Sterling
Feb. 2020 Preprint A Cubical Language for Bishop Sets
J. Sterling, C. Angiuli, and D. Gratzer


To appear Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
Journal of the ACM
J. Sterling, R. Harper
LICS '21
To appear Normalization for Cubical Type Theory
36th Annual Symposium on Logic in Computer Science
J. Sterling, C. Angiuli
JFP Higher order functions and Brouwer's Thesis
Journal of Functional Programming, Bob Harper Festschrift Collection
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.)

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
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

Lectures and Research Notes

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 (15-317) at CMU
Fall 2017 Lecture 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

Academic Service

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 long-term mentoring program for programming languges researchers (SIGPLAN-M).

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.