Jon Sterling

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

• My writings:
  • All publications, drafts, notes, and talks
  • My “Forest” where I organize my mathematical notes
  • Foundations of Relative Category Theory, a draft hypertext reference book
  • My old research blog
• My students
• Public topic bibliographies:
  • Bibliography of synthetic Tait computability
  • Bibliography of guarded domain theory
  • Bibliography of cubical type theory
• Translations of French category theory papers
• Inspiring quotations on science
• A declaration on inclusion in the homotopy type theory community
• Curriculum vitae

Recent News & Travel

Featured Talks

Recent Drafts

@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}
}

@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},
}

@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},
}

@unpublished{sterling:2022:generic,
  doi = {10.48550/ARXIV.2210.04202},
  author = {Sterling, Jonathan},
  title = {What should a generic object be?},
  year = {2022},
  note = {Unpublished manuscript},
}

@unpublished{sterling:2022:naive,
  author = {Sterling, Jonathan},
  year = {2022},
  month = jun,
  note = {Unpublished manuscript},
  title = {Na\"{i}ve logical relations in synthetic {Tait} computability},
}

@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

@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},
}

@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},
}

@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},
}

@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},
}

@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},
}

@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},
}

@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},
}

@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},
}

@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},
}

@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},
}

@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

@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}},
}

@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},
}

Funding & Grants

Academic Service

I am on the program committee for ICFP 2023 and HoTT/UF 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

Awards