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, 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).
- All publications, drafts, notes, and talks
- My Forest where I organize my mathematical notes
- My students
- Public topic bibliographies:
- Translations of French category theory papers
- Inspiring quotations on science
- A declaration on inclusion in the homotopy type theory community
- Curriculum vitae
Featured Talks
CATMI '23 | Category Theory at Work in Computational Mathematics and Theoretical Informatics June 2023 |
Apr. 2023 | Logic and Semantics Seminar, Aarhus University April 17, 2023 |
Recent Drafts
Mar. 2023 | March 27, 2023 |
Oct. 2022 | 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 | 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 | 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 | 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 | 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
See 9 older items
LMCS | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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, 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 | 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 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 |