Jon Sterling

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

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 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. '21	week-long visit to the University of Cambridge
Oct. 21, '21	awarded PhD by Carnegie Mellon University
Sep. '21	successfully defended my dissertation, moved to Aarhus
Jun. '21	accepted postdoctoral position working with L. Birkedal
Aug. '20	thesis proposal presented and accepted
Jul. '19	received ICFP '19 Distinguished Paper Award
Jun. '19	received 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)

abstract, announcement, slides

Doctoral Dissertation

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

Preprints & Recent Drafts

Dec. '21	PreprintBilimits in categories of partial maps abstract, local copy, citation
Dec. '20	PreprintSyntactic categories for dependent type theory: sketching and adequacy D. Gratzer, J. Sterling abstract, arXiv preprint, citation
Feb. '20	PreprintA Cubical Language for Bishop Sets J. Sterling, C. Angiuli, D. Gratzer abstract, arXiv preprint, citation

Refereed Publications

POPL '22	A cost-aware logical framework Y. Niu, J. Sterling, H. Grodin, R. Harper 49th ACM SIGPLAN Symposium on Principles of Programming Languages doi, abstract, announcement, arXiv preprint, artifact, citation
LICS '21	Normalization for Cubical Type theory J. Sterling, C. Angiuli 36th Annual Symposium on Logic in Computer Science doi, abstract, arXiv preprint, local copy, video, slides, citation
JFP	Higher order functions and Brouwer's Thesis Journal of Functional Programming, Bob Harper Festschrift Collection doi, abstract, arXiv preprint, artifact, citation
JACM	Logical Relations as Types: Proof-Relevant Parametricity for Program Modules J. Sterling, R. Harper Journal of the ACM doi, abstract, arXiv preprint, local copy, citation, errata
FSCD '19	Cubical Syntax for Reflection-Free Extensional Equality J. Sterling, C. Angiuli, D. Gratzer International Conference on Formal Structures for Computation and Deduction (FSCD), 2019 FSCD '19 Best Paper Award for Junior Researchers doi, abstract, arXiv preprint, slides, citation
ICFP '19	Implementing a Modal Dependent Type Theory D. Gratzer, J. Sterling, L. Birkedal International Conference on Functional Programming (ICFP), 2019 ICFP '19 Distinguished Paper Award doi, abstract, citation
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) doi, abstract, arXiv preprint, local copy, slides, citation
LEUS	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. doi, abstract, citation

Funding and Grants

AFOSR

Session Types and Phase Distinctions for Noninterference (2021)

Unfunded Collaborator

FA9550-21-1-0385

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) abstract, announcement, slides
Oct. 15, '21	Normalization for (Cartesian) Cubical Type Theory MURI Team Meeting 2021 slides
ML '21	A metalanguage for multi-phase modularity J. Sterling, R. Harper ML Family Workshop 2021 abstract, announcement, local copy, video, slides, citation
CT20→21	Normalization for cubical type theory J. Sterling, C. Angiuli Category Theory 2021 local copy, video, slides
Mar. '20	(Cubical) Computability Structures MURI Team Meeting 2020 slides
TYPES '19	XTT: Cubical Syntax for Extensional Equality (without equality reflection) J. Sterling, C. Angiuli, D. Gratzer TYPES 2019 announcement, slides
HoTT '19	Cubical Exact Equality and Categorical Gluing J. Sterling, C. Angiuli, D. Gratzer International Conference on Homotopy Type Theory, 2019 abstract, slides
Aug. '18	redtt: implementing cartesian cubical type theory C. Angiuli, E. Cavallo, Favonia, R. Harper, A. Mörtberg, J. Sterling Dagstuhl Seminar 18341: Formalization of Mathematics in Type Theory slides
LFMTP '18	The RedPRL Proof Assistant C. Angiuli, E. Cavallo, Favonia, R. Harper, J. Sterling International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), 2018 doi, abstract, citation

Seminar Talks

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

Teaching

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

Other Activities

Together with my co-hosts David Christiansen and Darin Morrison, I helped create The Type Theory Podcast.