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, and will be starting as an Associate Professor at University of Cambridge in Autumn; 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).

Featured Talks

Recent Drafts

Mar. 2023
Preprint Towards a geometry for syntax
March 27, 2023
Oct. 2022
Preprint Controlling unfolding in type theory
Under review
October 10, 2022
BibTeX citation
@unpublished{gratzer-sterling-angiuli-coquand-birkedal:2022,
  doi = {10.48550/ARXIV.2210.05420},
  author = {Gratzer, Daniel and Sterling, Jonathan and Angiuli, Carlo and Coquand, Thierry and Birkedal, Lars},
  title = {Controlling unfolding in type theory},
  year = {2022},
  note = {Unpublished manuscript}
}
Oct. 2022
Preprint Denotational semantics of general store and polymorphism
Under review
October 6, 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},
}
Oct. 2022
Preprint Reflections on existential types
October 1, 2022
BibTeX citation
@article{sterling:2022:existentials,
  doi = {10.48550/ARXIV.2210.00758},
  author = {Sterling, Jonathan},
  title = {Reflections on existential types},
  publisher = {arXiv},
  year = {2022},
  note = {Unpublished manuscript},
}
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},
}
See one older item
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

MSCS
What should a generic object be?
Mathematical Structures in Computer Science
April 25, 2023
BibTeX citation
@article{sterling:2023:generic,
  author = {Sterling, Jonathan},
  publisher = {Cambridge University Press},
  date = {2023},
  doi = {10.1017/S0960129523000117},
  journaltitle = {Mathematical Structures in Computer Science},
  pages = {1--22},
  title = {What should a generic object be?},
}
MFPS '23
To appear A denotationally-based program logic for higher-order store
F. L. Aagaard, J. Sterling, and L. Birkedal
39th International Conference on Mathematical Foundations of Programming Semantics
April 8, 2023
MFPS '22
Classifying topoi in synthetic guarded domain theory: the universal property of multi-clock guarded recursion
38th International Conference on Mathematical Foundations of Programming Semantics
February 22, 2023
BibTeX citation
@inproceedings{palombi-sterling:2023,
  author = {Palombi, Daniele and Sterling, Jonathan},
  booktitle = {Proceedings 38th Conference on Mathematical Foundations of Programming Semantics, {MFPS} 2022},
  year = {2023},
  month = feb,
  title = {Classifying topoi in synthetic guarded domain theory},
  doi = {10.46298/entics.10323},
}
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},
}
See 9 older items
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},
}
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
@online{sterling:2022:thesis:overview,
  author = {Sterling, Jonathan},
  url = {https://www.jonmsterling.com/forest/trees/jms-000q/},
  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},
}

Academic Service

I am on the program committee for ICFP 2023, HoTT/UF 2023, and WITS 2023; previously I served on the program committees for POPL 2023, 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