Jon Sterling

127 Turing
Department of Computer Science
Aarhus University
Aabogade 34
8200 Aarhus N, Denmark
jsterling@cs.au.dk
ORCID iD iconhttps://orcid.org/0000-0002-0585-5564

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, domain 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

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

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

Recent Drafts

Sep. 2022
Preprint Denotational semantics of general store and polymorphism
September 9, 2022
BibTeX citation
@unpublished{sterling-gratzer-birkedal:2022,
  author = {Sterling, Jonathan and Gratzer, Daniel and Birkedal, Lars},
  year = {2022},
  month = jul,
  note = {Unpublished manuscript},
  title = {Denotational semantics of general store and polymorphism},
}
Jul. 2022
Preprint What should a generic object be?
Under review
July 13, 2022
BibTeX citation
@unpublished{sterling:2022:generic,
  author = {Sterling, Jonathan},
  year = {2022},
  month = jul,
  note = {Unpublished manuscript},
  title = {What should a generic object be?},
}
Jun. 2022
Preprint Naïve logical relations in synthetic Tait computability
BibTeX citation
@unpublished{sterling:2022:naive,
  author = {Sterling, Jonathan},
  year = {2022},
  month = jun,
  note = {Unpublished manuscript},
  title = {Na\"{i}ve logical relations in synthetic {Tait} computability},
}
Feb. 2022
Preprint Strict universes for Grothendieck topoi
Under review
February 21, 2022
BibTeX citation
@unpublished{gratzer-shulman-sterling:2022:universes,
  author = {Gratzer, Daniel and Shulman, Michael and Sterling, Jonathan},
  year = {2022},
  month = feb,
  doi = {10.48550/arXiv.2202.12012},
  eprint = {2202.12012},
  eprintclass = {math.CT},
  eprinttype = {arXiv},
  note = {Unpublished manuscript},
  title = {Strict universes for Grothendieck topoi},
}

Recent Publications

FSCD '22
Sheaf semantics of termination-insensitive noninterference
International Conference on Formal Structures for Computation and Deduction (FSCD)
June 28, 2022
BibTeX citation
@inproceedings{sterling-harper:2022,
  author = {Sterling, Jonathan and Harper, Robert},
  editor = {Felty, Amy P.},
  address = {Dagstuhl, Germany},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  year = {2022},
  month = aug,
  doi = {10.4230/LIPIcs.FSCD.2022.5},
  eprint = {2204.09421},
  eprintclass = {cs.PL},
  eprinttype = {arXiv},
  isbn = {978-3-95977-233-4},
  issn = {1868-8969},
  pages = {5:1--5:19},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  title = {Sheaf semantics of termination-insensitive noninterference},
  volume = {228},
}
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
BibTeX citation
@inproceedings{palombi-sterling:2022,
  author = {Palombi, Daniele and Sterling, Jonathan},
  url = {https://www.jonmsterling.com/papers/palombi-sterling:2022.pdf},
  booktitle = {Proceedings 38th Conference on Mathematical Foundations of Programming Semantics, {MFPS} 2022},
  year = {2022},
  note = {To appear},
  title = {Classifying topoi in synthetic guarded domain theory},
}
LMCS
A Cubical Language for Bishop Sets
Logical Methods in Computer Science
February 9, 2022
BibTeX citation
@article{sterling-angiuli-gratzer:2022,
  author = {Sterling, Jonathan and Angiuli, Carlo and Gratzer, Daniel},
  year = {2022},
  month = mar,
  doi = {10.46298/lmcs-18(1:43)2022},
  eprint = {2003.01491},
  eprintclass = {cs.LO},
  eprinttype = {arXiv},
  issue = {1},
  journal = {Logical Methods in Computer Science},
  title = {{A Cubical Language for Bishop Sets}},
  volume = {18},
}
POPL '22
A cost-aware logical framework
49th ACM SIGPLAN Symposium on Principles of Programming Languages
January 2022
BibTeX citation
@article{niu-sterling-grodin-harper:2022,
  author = {Niu, Yue and Sterling, Jonathan and Grodin, Harrison and Harper, Robert},
  address = {New York, NY, USA},
  publisher = {Association for Computing Machinery},
  year = {2022},
  month = jan,
  doi = {10.1145/3498670},
  eprint = {2107.04663},
  eprintclass = {cs.PL},
  eprinttype = {arXiv},
  journal = {Proceedings of the ACM on Programming Languages},
  number = {POPL},
  title = {A Cost-Aware Logical Framework},
  volume = {6},
}
See 7 older publications
LICS '21
Normalization for Cubical Type theory
36th Annual Symposium on Logic in Computer Science
July 7, 2021
BibTeX citation
@inproceedings{sterling-angiuli:2021,
  author = {Sterling, Jonathan and Angiuli, Carlo},
  address = {Los Alamitos, CA, USA},
  publisher = {IEEE Computer Society},
  booktitle = {2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
  year = {2021},
  month = jul,
  doi = {10.1109/LICS52264.2021.9470719},
  eprint = {2101.11479},
  eprintclass = {cs.LO},
  eprinttype = {arXiv},
  pages = {1--15},
  title = {Normalization for Cubical Type Theory},
}
JFP
Higher order functions and Brouwer's Thesis
Journal of Functional Programming, Bob Harper Festschrift Collection
May 19, 2021
BibTeX citation
@article{sterling:2021:bhfs,
  author = {Sterling, Jonathan},
  publisher = {Cambridge University Press},
  date = {2021},
  doi = {10.1017/S0956796821000095},
  eprint = {1608.03814},
  eprintclass = {math.LO},
  eprinttype = {arXiv},
  journaltitle = {Journal of Functional Programming},
  note = {\emph{Bob Harper Festschrift Collection}},
  pages = {e11},
  title = {Higher order functions and Brouwer's thesis},
  volume = {31},
}
JACM
Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
Journal of the ACM
May 2021
BibTeX citation
@article{sterling-harper:2021,
  author = {Sterling, Jonathan and Harper, Robert},
  address = {New York, NY, USA},
  publisher = {Association for Computing Machinery},
  year = {2021},
  month = oct,
  doi = {10.1145/3474834},
  eprint = {2010.08599},
  eprintclass = {cs.PL},
  eprinttype = {arXiv},
  issn = {0004-5411},
  journal = {Journal of the ACM},
  number = {6},
  title = {Logical Relations as Types: Proof-Relevant Parametricity for Program Modules},
  volume = {68},
}
ICFP '19
Implementing a Modal Dependent Type Theory
International Conference on Functional Programming (ICFP), 2019
ICFP '19 Distinguished Paper Award
BibTeX citation
@article{gratzer-sterling-birkedal:2019,
  author = {Gratzer, Daniel and Sterling, Jonathan and Birkedal, Lars},
  location = {New York, NY, USA},
  publisher = {ACM},
  date = {2019-07},
  doi = {10.1145/3341711},
  issn = {2475-1421},
  journaltitle = {Proceedings of the ACM on Programming Languages},
  keywords = {Modal types,dependent types,normalization by evaluation,type-checking},
  number = {ICFP},
  pages = {107:1--107:29},
  title = {Implementing a Modal Dependent Type Theory},
  volume = {3},
}
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
BibTeX citation
@inproceedings{sterling-angiuli-gratzer:2019,
  author = {Sterling, Jonathan and Angiuli, Carlo and Gratzer, Daniel},
  editor = {Geuvers, Herman},
  location = {Dagstuhl, Germany},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  url = {http://drops.dagstuhl.de/opus/volltexte/2019/10538},
  booktitle = {Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  date = {2019},
  doi = {10.4230/LIPIcs.FSCD.2019.31},
  eprint = {1904.08562},
  eprinttype = {arXiv},
  isbn = {978-3-95977-107-8},
  issn = {1868-8969},
  pages = {31:1--31:25},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  title = {Cubical Syntax for Reflection-Free Extensional Equality},
  volume = {131},
}
LICS '18
Guarded Computational Type Theory
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18)
BibTeX citation
@inproceedings{sterling-harper:2018,
 author = {Sterling, Jonathan and Harper, Robert},
 title = {Guarded Computational Type Theory},
 booktitle = {Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science},
 series = {LICS '18},
 year = {2018},
 isbn = {978-1-4503-5583-4},
 location = {Oxford, United Kingdom},
 pages = {879--888},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/3209108.3209153},
 doi = {10.1145/3209108.3209153},
 acmid = {3209153},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {clocks, dependent types, guarded recursion, operational semantics, type theory},
}
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.
BibTeX citation
@inbook{valentine-sterling:2016,
  author={Valentine, Rebecca and Sterling, Jonathan},
  editor={Redmond, Juan and Pombo Martins, Olga and Nepomuceno Fern{\'a}ndez, {\'A}ngel},
  title={Dependent Types for Pragmatics},
  booktitle={Epistemology, Knowledge and the Impact of Interaction},
  year={2016},
  publisher={Springer International Publishing},
  address={Cham},
  pages={123--139},
  isbn={978-3-319-26506-3},
  doi={10.1007/978-3-319-26506-3_4},
}

Doctoral Dissertation

Apr. 2022
Dissertation Overview: First Steps in Synthetic Tait Computability
Dissertation Overview, Carnegie Mellon University
BibTeX citation
@unpublished{sterling:2022:thesis:overview,
  author = {Sterling, Jonathan},
  url = {https://www.jonmsterling.com/papers/sterling:2022:thesis:overview.pdf},
  year = {2022},
  month = apr,
  note = {Synopsis of doctoral dissertation, Carnegie Mellon University},
  title = {Dissertation Overview: \emph{First Steps in Synthetic {Tait} Computability}},
}
Sep. 2021
First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory
Doctoral Dissertation, Carnegie Mellon University
September 13, 2021
BibTeX citation
@phdthesis{sterling:2021:thesis,
  author = {Sterling, Jonathan},
  school = {Carnegie Mellon University},
  year = {2021},
  doi = {10.5281/zenodo.6990769},
  note = {Version 1.1, revised May 2022},
  number = {CMU-CS-21-142},
  title = {First Steps in Synthetic {Tait} Computability: The Objective Metatheory of Cubical Type Theory},
}

Students

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.

The theses I am involved in are listed below.

Daniele Palombi (Bachelor)
Department of Mathematics
Sapienza Università di Roma
Topic: Synthetic guarded domain theory
Role: external co-supervisor
Aoyang Yu (Bachelor)
College of Computer Science and Technology
Zhejiang University
Topic: Type theory
Role: external supervisor
Yue Niu (PhD)
Computer Science Department
Carnegie Mellon University
Topic: A cost-aware logical framework
Role: thesis committee member

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

Teaching

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

Awards

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