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 L. Birkedal; I earned my PhD from Carnegie Mellon University under R. 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 Bibliography 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 enable both programmers and mathematicians to negotiate the different levels of abstraction that arise in their work. I apply my research to interactive theorem provers, global safety and security properties of programming languages, and higher-dimensional mathematics (homotopy theory).

My doctoral dissertation was about 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 & Travel

Nov. '21week-long visit to the University of Cambridge
Oct. 21, '21awarded PhD by Carnegie Mellon University
Sep. '21successfully defended my dissertation, moved to Aarhus
Jun. '21accepted postdoctoral position working with L. Birkedal
Aug. '20thesis proposal presented and accepted
Jul. '19received ICFP '19 Distinguished Paper Award
Jun. '19received FSCD '19 Best Paper Award for Junior Researchers

Upcoming & Recent Presentations

WITS '22
Make Three To Throw Away: Frontiers in Homotopical Proof Assistants
Workshop on the Implementation of Type Systems (keynote)

Doctoral Dissertation

Sep. 13, '21
First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory
Doctoral Dissertation, Carnegie Mellon University
Aug. '20
Objective Metatheory of (Cubical) Type Theories
Doctoral Thesis Proposal, Carnegie Mellon University

Preprints & Recent Drafts

Dec. '21
PreprintBilimits in categories of partial maps
Dec. '20
PreprintSyntactic categories for dependent type theory: sketching and adequacy
Feb. '20
PreprintA Cubical Language for Bishop Sets

Refereed Publications

POPL '22
A cost-aware logical framework
49th ACM SIGPLAN Symposium on Principles of Programming Languages
LICS '21
Normalization for Cubical Type theory
36th Annual Symposium on Logic in Computer Science
Higher order functions and Brouwer's Thesis
Journal of Functional Programming, Bob Harper Festschrift Collection
Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
Journal of the ACM
FSCD '19
Cubical Syntax for Reflection-Free Extensional Equality
International Conference on Formal Structures for Computation and Deduction (FSCD), 2019
FSCD '19 Best Paper Award for Junior Researchers
ICFP '19
Implementing a Modal Dependent Type Theory
International Conference on Functional Programming (ICFP), 2019
ICFP '19 Distinguished Paper Award
LICS '18
Guarded Computational Type Theory
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18)
Dependent Types for Pragmatics
R. Valentine, 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, 2022), LICS (2017, 2021); and as a referee for Compositionality, LMCS and MSCS.

Workshop Talks

WITS '22
Make Three To Throw Away: Frontiers in Homotopical Proof Assistants
Workshop on the Implementation of Type Systems (keynote)
Oct. 15, '21
Normalization for (Cartesian) Cubical Type Theory
MURI Team Meeting 2021
ML '21
A metalanguage for multi-phase modularity
Normalization for cubical type theory
Mar. '20
(Cubical) Computability Structures
MURI Team Meeting 2020
XTT: Cubical Syntax for Extensional Equality (without equality reflection)
TYPES 2019
HoTT '19
Cubical Exact Equality and Categorical Gluing
International Conference on Homotopy Type Theory, 2019
Aug. '18
redtt: implementing cartesian cubical type theory
Dagstuhl Seminar 18341: Formalization of Mathematics in Type Theory
The RedPRL Proof Assistant
International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), 2018

Seminar Talks

Nov. 19, '21
Towards a geometry for syntax
Computer Laboratory, University of Cambridge
Nov. 1, '21
Between abstraction and composition...
Logic and Semantics Seminar, Aarhus University
Aug. 24, '21
Abstraction, composition, and the phase distinction
CMU Speakers Club
May '21
Normalization for Cubical Type Theory
Padova Logic Seminar
Apr. '21
Logical Relations As Types
CCS Colloquium, Augusta University
Feb. '21
Normalization for Cubical Type theory
Pittsburgh's HoTT Seminar
Jun. '20
redtt and the future of Cartesian cubical type theory
Every Proof Assistant
Mar. '20
Objective Metatheory of Dependent Type Theories
Homotopy Type Theory Electronic Seminar Talks
Jan. '20
Gluing Models of Type Theory Along Flat Functors
CMU HoTT Seminar
Apr. '19
Algebraic Type Theory and the Gluing Construction
CMU HoTT Seminar


Fall 2018TA for Constructive Logic (15-317) with K. Crary
Fall 2017TA for Constructive Logic (15-317) with F. 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.