Jon Sterling

215 Ada
Department of Computer Science
Aarhus University
Aabogade 34
8200 Aarhus N, Denmark
jsterling@cs.au.dk

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.

Research

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

Jun. 2022	week-long scientific visit to IRIF hosted by A. Guatto
Mar. 2022	awarded the MSCA European postdoctoral fellowship
Mar. 2022	joined the program committees for POPL'23, ACT'22, and TyDE'22
Nov. 2021	week-long visit to the University of Cambridge hosted by J. Vicary
Oct. 2021	awarded PhD by Carnegie Mellon University
Sep. 2021	successfully defended my doctoral dissertation, moved to Aarhus
Jun. 2021	accepted postdoctoral position working with L. 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 & Recent Presentations

WG6	Invited Naïve logical relations in synthetic Tait computability WG6 kick-off meeting: Syntax and Semantics of Type Theories abstract, external link, local copy, citation May 20, 2022
Apr. 2022	Invited Intrinsic semantics of termination-insensitive noninterference Boston University POPV Seminar abstract, external link, slides April 26, 2022

Preprints & Recent Drafts

Apr. 2022	Preprint Classifying topoi in synthetic guarded domain theory: the universal property of multi-clock guarded recursion D. Palombi and J. Sterling abstract, local copy, citation April 19, 2022
Apr. 2022	Preprint What should a generic object be? J. Sterling abstract, local copy April 9, 2022
Feb. 2022	Preprint Strict universes for Grothendieck topoi D. Gratzer, M. Shulman, and J. Sterling Under review doi, abstract, arXiv preprint, local copy, citation February 21, 2022

Refereed Publications

FSCD '22	To appear Sheaf semantics of termination-insensitive noninterference J. Sterling and R. Harper International Conference on Formal Structures for Computation and Deduction (FSCD) doi, abstract, arXiv preprint, local copy, citation, errata April 19, 2022
LMCS	A Cubical Language for Bishop Sets J. Sterling, C. Angiuli, and D. Gratzer Logical Methods in Computer Science doi, abstract, arXiv preprint, local copy, citation February 9, 2022
POPL '22	A cost-aware logical framework Y. Niu, J. Sterling, H. Grodin, and R. Harper 49th ACM SIGPLAN Symposium on Principles of Programming Languages doi, abstract, external link, arXiv preprint, artifact, citation January 2022
LICS '21	Normalization for Cubical Type theory J. Sterling and C. Angiuli 36th Annual Symposium on Logic in Computer Science doi, abstract, arXiv preprint, local copy, video, slides, citation July 7, 2021
JFP	Higher order functions and Brouwer's Thesis J. Sterling Journal of Functional Programming, Bob Harper Festschrift Collection doi, abstract, arXiv preprint, artifact, citation May 19, 2021
JACM	Logical Relations as Types: Proof-Relevant Parametricity for Program Modules J. Sterling and R. Harper Journal of the ACM doi, abstract, arXiv preprint, local copy, citation, errata May 2021
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 doi, abstract, citation
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) FSCD '19 Best Paper Award for Junior Researchers doi, abstract, arXiv preprint, slides, citation
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) doi, abstract, arXiv preprint, local copy, slides, citation
LEUS	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. doi, abstract, citation

Doctoral Dissertation

Apr. 2022	Dissertation Overview: First Steps in Synthetic Tait Computability Dissertation Overview, Carnegie Mellon University local copy, citation
Sep. 2021	First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory Doctoral Dissertation, Carnegie Mellon University doi, abstract, external link, local copy, video, slides, citation, errata September 13, 2021
Aug. 2020	Objective Metatheory of (Cubical) Type Theories Doctoral Thesis Proposal, Carnegie Mellon University abstract, external link, local copy, slides

Supervision

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	TypeSynth: Synthetic Methods in Program Verification (2022) MSCA Postdoctoral Fellow Marie Skłodowska-Curie Actions Postdoctoral Fellowship
AFOSR	Session Types and Phase Distinctions for Noninterference (2021) Unfunded Collaborator Air Force Office of Scientific Research FA9550-21-1-0385

Academic service

I am on the program committee for POPL '2023, ACT'22, 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 J. Sterling doi, abstract, arXiv preprint, local copy, citation February 17, 2022
Feb. 2022	Notes The directed plump ordering D. Gratzer, M. Shulman, and J. Sterling doi, abstract, arXiv preprint, local copy, artifact, citation February 15, 2022
Dec. 2020	Notes Syntactic categories for dependent type theory: sketching and adequacy D. Gratzer and J. Sterling abstract, arXiv preprint, citation
Sep. 2018	Notes Normalization by gluing for free λ-theories J. Sterling and B. Spitters arXiv preprint, citation

Workshop Talks

WG6	Invited Naïve logical relations in synthetic Tait computability WG6 kick-off meeting: Syntax and Semantics of Type Theories abstract, external link, local copy, citation May 20, 2022
WITS '22	Invited Make Three To Throw Away: Frontiers in Homotopical Proof Assistants Workshop on the Implementation of Type Systems (keynote) abstract, external link, video, slides January 22, 2022
MURI'21	Normalization for (Cartesian) Cubical Type Theory MURI Team Meeting 2021 slides October 15, 2021
CT20→21	Normalization for cubical type theory J. Sterling and C. Angiuli Category Theory 2021 local copy, video, slides
ML '21	A metalanguage for multi-phase modularity J. Sterling and R. Harper ML Family Workshop 2021 abstract, external link, local copy, video, slides, citation
MURI'20	(Cubical) Computability Structures MURI Team Meeting 2020 slides March 2020
HoTT '19	Cubical Exact Equality and Categorical Gluing J. Sterling, C. Angiuli, and D. Gratzer International Conference on Homotopy Type Theory, 2019 abstract, slides
TYPES '19	XTT: Cubical Syntax for Extensional Equality (without equality reflection) J. Sterling, C. Angiuli, and D. Gratzer TYPES 2019 external link, slides
Aug. 2018	Invited 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 slides
LFMTP '18	Invited The RedPRL Proof Assistant C. Angiuli, E. Cavallo, Favonia, R. Harper, and J. Sterling International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), 2018 doi, abstract, citation

Seminar Talks

Apr. 2022	Invited Intrinsic semantics of termination-insensitive noninterference Boston University POPV Seminar abstract, external link, slides April 26, 2022
Nov. 2021	Invited Towards a geometry for syntax Computer Laboratory, University of Cambridge abstract, external link, slides November 19, 2021
Nov. 2021	Between abstraction and composition... Logic and Semantics Seminar, Aarhus University abstract, external link, slides November 1, 2021
Aug. 2021	Abstraction, composition, and the phase distinction CMU Speakers Club abstract, external link, slides August 24, 2021
May 2021	Invited Normalization for Cubical Type Theory J. Sterling and C. Angiuli Padova Logic Seminar abstract, external link
Apr. 2021	Invited Logical Relations As Types CCS Colloquium, Augusta University abstract, external link, video, slides
Feb. 2021	Normalization for Cubical Type theory J. Sterling and C. Angiuli Pittsburgh's HoTT Seminar abstract, external link
Jun. 2020	Invited redtt and the future of Cartesian cubical type theory Every Proof Assistant abstract, external link, video
Mar. 2020	Invited Objective Metatheory of Dependent Type Theories Homotopy Type Theory Electronic Seminar Talks abstract, external link, video, slides
Jan. 2020	Gluing Models of Type Theory Along Flat Functors J. Sterling and C. Angiuli CMU HoTT Seminar abstract, local copy
Apr. 2019	Algebraic Type Theory and the Gluing Construction CMU HoTT Seminar local copy

Teaching

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

Awards

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