Jon Sterling

215 Ada
Department of Computer Science
Aarhus University
Aabogade 34
8200 Aarhus N, Denmark
ORCID iD icon

I am a postdoctoral fellow at Aarhus University in the Logic and Semantics group supervised by Lars Birkedal; I am currently finishing my PhD at Carnegie Mellon University under Robert Harper. I study programming languages and semantics using type theory, category theory, and topos theory as a guide. 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. Research Blog Curriculum Vitae


Central to both the design of programming languages and the practice of software engineering is the tension between abstraction and composition. I employ semantic methods to design, verify, and implement languages and tools that both enable programmers and mathematicians to negotiate the different levels of abstraction that arise in their work. I apply my research to security qua information flow control, interactive theorem provers, global safety properties of programming languages, and higher-dimensional mathematics (homotopy theory).

My most recent and significant result is the proof of normalization and decidability of definitional equality for cubical type theory, a computational version of Homotopy Type Theory. My colleagues and I have also developed the redtt and cooltt proof assistants for Cartesian cubical type theory.

Recent News

Sep. 2021successfully defended my dissertation
Jun. 2021accepted postdoctoral position working with Lars Birkedal
Aug. 2020thesis proposal presented and accepted
Jul. 2019received ICFP '19 Distinguished Paper Award
Jun. 2019received FSCD '19 Best Paper Award for Junior Researchers

Recent Drafts

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


To appearLogical Relations as Types: Proof-Relevant Parametricity for Program Modules
J. Sterling, R. Harper
Journal of the ACM
LICS '21
Normalization for Cubical Type theory
J. Sterling, C. Angiuli
36th Annual Symposium on Logic in Computer Science
Higher order functions and Brouwer's Thesis
J. Sterling
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
ICFP '19 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
FSCD '19 Best Paper Award for Junior Researchers
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
LICS '18
Guarded Computational Type Theory
J. Sterling and R. Harper
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18)
Dependent Types for Pragmatics
D. McAdams and J. Sterling
In: 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.

Funding and Grants

Session Types and Phase Distinctions for Noninterference (2021)
Unfunded Collaborator
Air Force Office of Scientific Research

Academic Service

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

Workshop Talks

Normalization for cubical type theory
J. Sterling and C. Angiuli
ML '21
A metalanguage for multi-phase modularity
J. Sterling and R. Harper
HoTT '19
Cubical Exact Equality and Categorical Gluing
J. Sterling, C. Angiuli, and D. Gratzer
International Conference on Homotopy Type Theory, 2019
XTT: Cubical Syntax for Extensional Equality (without equality reflection)
J. Sterling, C. Angiuli, and D. Gratzer
TYPES 2019

Other Talks

Sep. 2021
First Steps in Synthetic Tait Computability
Doctoral Defense, Carnegie Mellon University
Aug. 2021
Abstraction, composition, and the phase distinction
CMU Speakers Club
May 2021
Normalization for Cubical Type Theory
Padova Logic Seminar
Apr. 2021
Logical Relations As Types
Feb. 2021
Normalization for Cubical Type theory
Aug. 2020
Objective Metatheory of (Cubical) Type Theories
Thesis Proposal
Jun. 2020
redtt and the future of Cartesian cubical type theory
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
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


Fall 2018TA for Constructive Logic (15-317) with Karl Crary
Fall 2017TA for Constructive Logic (15-317) with Frank Pfenning


2019ICFP '19 Distinguished Paper Award
2019FSCD '19 Best Paper Award for Junior Researchers
2011W.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.