Jon Sterling

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

I am a Marie Skłodowska-Curie Postdoctoral Fellow hosted at Aarhus University in the Logic and Semantics group 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

I am writing an online book on relative category theory!

Read my declaration on inclusion in the homotopy type theory community.


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

One of the main topics of my research is synthetic Tait computability, a type theoretic internal language that can be used to define logical relations. I am also interested in guarded domain theory and cubical type theory. I have compiled a list of inspiring quotations on science that have influenced my thinking and my work.

My coauthors are Carlo Angiuli, Lars Birkedal, Evan Cavallo, Daniel Gratzer, Harrison Grodin, Robert Harper, Favonia, Anders Mörtberg, Yue Niu, Daniele Palombi, Michael Shulman, Bas Spitters, and Rebecca Valentine.

Recent News & Travel

Aug. 2022joined the ICFP '23 program committee
Jul. 2022awarded runner-up for Beth Outstanding Dissertation Prize
Jun. 2022week-long scientific visit to IRIF hosted by A. Guatto
Mar. 2022awarded the MSCA European postdoctoral fellowship
Mar. 2022joined the program committees for POPL '23, ACT '22, and TyDE '22
Nov. 2021week-long visit to the University of Cambridge hosted by J. Vicary
Oct. 2021awarded PhD by Carnegie Mellon University
Sep. 2021successfully defended my doctoral dissertation, moved to Aarhus
Jun. 2021accepted postdoctoral position working with L. Birkedal
Aug. 2020thesis proposal presented and accepted
Jul. 2019received ICFP '19 Distinguished Paper Award
Jun. 2019received FSCD '19 Best Paper Award for Junior Researchers

Upcoming & Recent Presentations

InvitedComing soon How to code your own type theory
Colloquium, HoTTEST Summer School 2022
August 22, 2022
MURI '22
Invited Sheaf semantics of termination-insensitive noninterference
MURI Team Meeting 2022
June 30, 2022

Preprints & Recent Drafts

Jul. 2022
Preprint What should a generic object be?
Under review
July 13, 2022
Jul. 2022
Preprint Denotational semantics of general store and polymorphism
Jun. 2022
Preprint Naïve logical relations in synthetic Tait computability
Feb. 2022
Preprint Strict universes for Grothendieck topoi
Under review
February 21, 2022
Dec. 2020
Preprint Syntactic categories for dependent type theory: sketching and adequacy

Refereed Publications

FSCD '22
Sheaf semantics of termination-insensitive noninterference
International Conference on Formal Structures for Computation and Deduction (FSCD)
June 28, 2022
MFPS '22
To appear Classifying topoi in synthetic guarded domain theory: the universal property of multi-clock guarded recursion
38th International Conference on Mathematical Foundations of Programming Semantics
April 19, 2022
A Cubical Language for Bishop Sets
Logical Methods in Computer Science
February 9, 2022
POPL '22
A cost-aware logical framework
49th ACM SIGPLAN Symposium on Principles of Programming Languages
January 2022
LICS '21
Normalization for Cubical Type theory
36th Annual Symposium on Logic in Computer Science
July 7, 2021
Higher order functions and Brouwer's Thesis
Journal of Functional Programming, Bob Harper Festschrift Collection
May 19, 2021
Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
Journal of the ACM
May 2021
ICFP '19
Implementing a Modal Dependent Type Theory
International Conference on Functional Programming (ICFP), 2019
ICFP '19 Distinguished Paper Award
FSCD '19
Cubical Syntax for Reflection-Free Extensional Equality
International Conference on Formal Structures for Computation and Deduction (FSCD)
FSCD '19 Best Paper Award for Junior Researchers
LICS '18
Guarded Computational Type Theory
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18)
Invited Dependent Types for Pragmatics
R. Valentine 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.

Doctoral Dissertation

Apr. 2022
Dissertation Overview: First Steps in Synthetic Tait Computability
Dissertation Overview, Carnegie Mellon University
Sep. 2021
First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory
Doctoral Dissertation, Carnegie Mellon University
September 13, 2021
Aug. 2020
Objective Metatheory of (Cubical) Type Theories
Doctoral Thesis Proposal, Carnegie Mellon University


I am willing to supervise bachelors and masters’ theses on any topic within my area of expertise; this includes type theory, programming languages, topos theory, domain theory, proof assistants, etc. If your university allows it, then I am open to (co-)supervising students at institutions other than my own. If you have any questions, feel free to contact me.

My supervisees

Daniele Palombi (Bachelor)
Department of Mathematics
Sapienza Università di Roma
Topic: Synthetic Guarded Domain Theory
My Role: external co-supervisor

Funding & Grants

MSCA Postdoctoral Fellow
Marie Skłodowska-Curie Actions Postdoctoral Fellowship
Session Types and Phase Distinctions for Noninterference (2021)
Unfunded Collaborator
Air Force Office of Scientific Research

Academic Service

I am on the program committees for POPL 2023 and ICFP 2023; previously I served on the program committees for ACT 2022, and TyDe 2022.

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

Research Notes

Feb. 2022
Notes Bilimits in categories of partial maps
February 17, 2022
Feb. 2022
Notes The directed plump ordering
February 15, 2022
Sep. 2018
Notes Normalization by gluing for free λ-theories

Workshop Talks

MURI '22
Invited Sheaf semantics of termination-insensitive noninterference
MURI Team Meeting 2022
June 30, 2022
Invited Naïve logical relations in synthetic Tait computability
WG6 kick-off meeting: Syntax and Semantics of Type Theories
May 20, 2022
WITS '22
Invited Make Three To Throw Away: Frontiers in Homotopical Proof Assistants
Workshop on the Implementation of Type Systems (keynote)
January 22, 2022
MURI '21
Normalization for (Cartesian) Cubical Type Theory
MURI Team Meeting 2021
October 15, 2021
Normalization for cubical type theory
ML '21
A metalanguage for multi-phase modularity
MURI '20
(Cubical) Computability Structures
MURI Team Meeting 2020
March 2020
HoTT '19
Cubical Exact Equality and Categorical Gluing
International Conference on Homotopy Type Theory, 2019
XTT: Cubical Syntax for Extensional Equality (without equality reflection)
TYPES 2019
Aug. 2018
Invited redtt: implementing cartesian cubical type theory
Dagstuhl Seminar 18341: Formalization of Mathematics in Type Theory
Invited The RedPRL Proof Assistant
International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), 2018

Seminar Talks

Jun. 2022
Invited Naïve logical relations in synthetic Tait computability
Proofs, Programs and Systems seminar (IRIF PPS)
June 9, 2022
Apr. 2022
Invited Intrinsic semantics of termination-insensitive noninterference
Boston University POPV Seminar
April 26, 2022
Nov. 2021
Invited Towards a geometry for syntax
Computer Laboratory, University of Cambridge
November 19, 2021
Nov. 2021
Between abstraction and composition...
Logic and Semantics Seminar, Aarhus University
November 1, 2021
Aug. 2021
Abstraction, composition, and the phase distinction
CMU Speakers Club
August 24, 2021
May 2021
Invited Normalization for Cubical Type Theory
Padova Logic Seminar
Apr. 2021
Invited Logical Relations As Types
CCS Colloquium, Augusta University
Feb. 2021
Normalization for Cubical Type theory
Pittsburgh's HoTT Seminar
Jun. 2020
Invited redtt and the future of Cartesian cubical type theory
Every Proof Assistant
Mar. 2020
Invited Objective Metatheory of Dependent Type Theories
Homotopy Type Theory Electronic Seminar Talks
Jan. 2020
Gluing Models of Type Theory Along Flat Functors
CMU HoTT Seminar
Apr. 2019
Algebraic Type Theory and the Gluing Construction
CMU HoTT Seminar

Lectures & Colloquia

InvitedComing soon How to code your own type theory
Colloquium, HoTTEST Summer School 2022
August 22, 2022


Fall 2022Category Theory with Lars Birkedal and Alejandro Aguirre
Fall 2018TA for Constructive Logic (15-317) with Karl Crary
Fall 2017TA for Constructive Logic (15-317) with Frank Pfenning


2022Runner Up, Beth Outstanding Dissertation Prize
2019ICFP '19 Distinguished Paper Award
2019FSCD '19 Best Paper Award for Junior Researchers
2011W.K. Pritchett Prize in Elementary Greek, UC Berkeley