Jon Sterling
Department of Computer Science
Aarhus University
Aabogade 34
8200 Aarhus N, Denmark
jsterling@cs.au.dk
Table of contents
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
Jul. 2022 | awarded runner-up for Beth Outstanding Dissertation Prize |
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
HoTTEST | Colloquium, HoTTEST Summer School 2022 August 22, 2022 |
MURI '22 | MURI Team Meeting 2022 June 30, 2022 |
Preprints & Recent Drafts
Jul. 2022 | Under review July 13, 2022 |
Jul. 2022 | |
Jun. 2022 | |
Feb. 2022 | Under review February 21, 2022 |
Dec. 2020 |
Refereed Publications
Doctoral Dissertation
Apr. 2022 | Dissertation Overview, Carnegie Mellon University |
Sep. 2021 | Doctoral Dissertation, Carnegie Mellon University September 13, 2021 |
Aug. 2020 | Doctoral Thesis Proposal, Carnegie Mellon University |
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 | 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; 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 | February 17, 2022 |
Feb. 2022 | February 15, 2022 |
Sep. 2018 |
Workshop Talks
MURI '22 | MURI Team Meeting 2022 June 30, 2022 |
WG6 | WG6 kick-off meeting: Syntax and Semantics of Type Theories May 20, 2022 |
WITS '22 | Workshop on the Implementation of Type Systems (keynote) January 22, 2022 |
MURI '21 | MURI Team Meeting 2021 October 15, 2021 |
CT20→21 | |
ML '21 | |
MURI '20 | MURI Team Meeting 2020 March 2020 |
HoTT '19 | International Conference on Homotopy Type Theory, 2019 |
TYPES '19 | TYPES 2019 |
Aug. 2018 | Dagstuhl Seminar 18341: Formalization of Mathematics in Type Theory |
LFMTP '18 | International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), 2018 |
Seminar Talks
Jun. 2022 | Proofs, Programs and Systems seminar (IRIF PPS) June 9, 2022 |
Apr. 2022 | Boston University POPV Seminar April 26, 2022 |
Nov. 2021 | Computer Laboratory, University of Cambridge November 19, 2021 |
Nov. 2021 | Logic and Semantics Seminar, Aarhus University November 1, 2021 |
Aug. 2021 | CMU Speakers Club August 24, 2021 |
May 2021 | Padova Logic Seminar |
Apr. 2021 | CCS Colloquium, Augusta University |
Feb. 2021 | Pittsburgh's HoTT Seminar |
Jun. 2020 | Every Proof Assistant |
Mar. 2020 | Homotopy Type Theory Electronic Seminar Talks |
Jan. 2020 | CMU HoTT Seminar |
Apr. 2019 | CMU HoTT Seminar |
Lectures & Colloquia
HoTTEST | Colloquium, HoTTEST Summer School 2022 August 22, 2022 |
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
2022 | Runner Up, Beth Outstanding Dissertation Prize |
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 |