Bibliography of Jon Sterling
Table of contents
The following authors are represented in this bibliography: Carlo Angiuli, Lars Birkedal, Evan Cavallo, Thierry Coquand, Daniel Gratzer, Harrison Grodin, Robert Harper, Favonia, Anders Mörtberg, Yue Niu, Daniele Palombi, Michael Shulman, Bas Spitters, Jonathan Sterling, and Rebecca Valentine.
Refereed Publications
Unpublished Manuscripts
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}, } |
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}, } |
Workshop Presentations
FICS '23 | Fixed Points in Computer Science 2023 February 17, 2023 |
Dec. 2022 | Workshop on Dependent Type Theory (to celebrate the Defense of Loïc Pujet) December 14, 2022 |
MURI '22 | MURI Team Meeting 2022 June 30, 2022 BibTeX citation@misc{sterling-harper:2022:muri, author = {Sterling, Jonathan and Harper, Robert}, url = {https://www.jonmsterling.com/slides/sterling:2022:muri.pdf}, year = {2022}, month = jun, note = {Talk given at the 2022 MURI Team Meeting}, title = {Sheaf semantics of termination-insensitive noninterference}, } |
WG6 | WG6 kick-off meeting: Syntax and Semantics of Type Theories May 20, 2022 BibTeX citation@misc{sterling:2022:wg6, author = {Sterling, Jonathan}, year = {2022}, month = may, note = {WG6 kick-off meeting: Syntax and Semantics of Type Theories (Invited Talk)}, title = {Na\"{i}ve logical relations in synthetic {Tait} computability}, } |
WITS '22 | Workshop on the Implementation of Type Systems (keynote) January 22, 2022 |
MURI '21 | MURI Team Meeting 2021 October 15, 2021 |
ML '21 | BibTeX citation@unpublished{sterling-harper:2021:mlw, author = {Sterling, Jonathan and Harper, Robert}, url = {https://icfp21.sigplan.org/details/mlfamilyworkshop-2021-papers/5/A-metalanguage-for-multi-phase-modularity}, year = {2021}, month = aug, note = {ML 2021 abstract and talk}, title = {A metalanguage for multi-phase modularity}, } |
CT20→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 BibTeX citation@inproceedings{redprl:2018:lfmtp, author = {Angiuli, Carlo and Cavallo, Evan and {Hou (Favonia)}, Kuen-Bang and Harper, Robert and Sterling, Jonathan}, editor = {Blanqui, Fr\'{e}d\'{e}ric and Reis, Giselle}, publisher = {Open Publishing Association}, booktitle = {Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2018, Oxford, UK, 7th July 2018.}, date = {2018}, doi = {10.4204/EPTCS.274.1}, pages = {1--10}, title = {{The \textsf{\textcolor[rgb]{.91,.31,.27}{Red}PRL} Proof Assistant (Invited Paper)}}, } |
Dissertations
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}, } |
Research Notes
Oct. 2022 | October 14, 2022 |
Feb. 2022 | February 17, 2022 BibTeX citation@unpublished{sterling:2022:bilimits, author = {Sterling, Jonathan}, year = {2022}, month = feb, doi = {10.48550/arXiv.2202.08657}, eprint = {2202.08657}, eprintclass = {cs.LO}, eprinttype = {arXiv}, title = {Bilimits in categories of partial maps}, } |
Feb. 2022 | February 15, 2022 BibTeX citation@unpublished{gratzer-shulman-sterling:2022:plump, author = {Gratzer, Daniel and Shulman, Michael and Sterling, Jonathan}, year = {2022}, doi = {10.48550/arXiv.2202.07329}, eprint = {2202.07329}, eprintclass = {cs.LO}, eprinttype = {arXiv}, title = {The directed plump ordering}, } |
Dec. 2020 | BibTeX citation@unpublished{gratzer-sterling:2020, author = {Gratzer, Daniel and Sterling, Jonathan}, year = {2020}, eprint = {2012.10783}, eprintclass = {cs.LO}, eprinttype = {arXiv}, title = {Syntactic categories for dependent type theory: sketching and adequacy}, } |
Sep. 2018 | BibTeX citation@unpublished{sterling-spitters:2018, author = {Sterling, Jonathan and Spitters, Bas}, year = {2018}, month = sep, eprint = {1809.08646}, eprintclass = {cs.LO}, eprinttype = {arXiv}, title = {Normalization by gluing for free $\lambda$-theories}, } |
Seminar Talks
Feb. 2023 | Cambridge Computer Laboratory, University of Cambridge February 9, 2023 |
Feb. 2023 | University of Birmingham February 2, 2023 |
Nov. 2022 | Programming, Logic and Semantics, ITU Copenhagen November 8, 2022 |
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 |
HoTTEST | Homotopy Type Theory Electronic Seminar Talks March 2020 |
Jan. 2020 | CMU HoTT Seminar |
Apr. 2019 | CMU HoTT Seminar |
Lectures
HoTTEST | Colloquium, HoTTEST Summer School 2022 August 22, 2022 |