Bibliography of Jon Sterling

The following authors are represented in this bibliography: Carlo Angiuli, Lars Birkedal, Evan Cavallo, 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

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

Unpublished Manuscripts

Oct. 2022
Coming soonPreprint Reflections on existential types
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},
}

Workshop Presentations

MURI '22
Invited Sheaf semantics of termination-insensitive noninterference
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
Invited Naïve logical relations in synthetic Tait computability
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
Invited Make Three To Throw Away: Frontiers in Homotopical Proof Assistants
Workshop on the Implementation of Type Systems (keynote)
January 22, 2022
MURI '21
Normalization for (Cartesian) Cubical Type Theory
MURI Team Meeting 2021
October 15, 2021
CT2021
Normalization for cubical type theory
ML '21
A metalanguage for multi-phase modularity
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},
}
MURI '20
(Cubical) Computability Structures
MURI Team Meeting 2020
March 2020
HoTT '19
Cubical Exact Equality and Categorical Gluing
International Conference on Homotopy Type Theory, 2019
TYPES '19
XTT: Cubical Syntax for Extensional Equality (without equality reflection)
TYPES 2019
Aug. 2018
Invited redtt: implementing cartesian cubical type theory
Dagstuhl Seminar 18341: Formalization of Mathematics in Type Theory
LFMTP '18
Invited The RedPRL Proof Assistant
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: 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},
}

Research Notes

Feb. 2022
Notes Bilimits in categories of partial maps
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
Notes The directed plump ordering
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
Notes Syntactic categories for dependent type theory: sketching and adequacy
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
Notes Normalization by gluing for free λ-theories
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

Jun. 2022
Invited Naïve logical relations in synthetic Tait computability
Proofs, Programs and Systems seminar (IRIF PPS)
June 9, 2022
Apr. 2022
Invited Intrinsic semantics of termination-insensitive noninterference
Boston University POPV Seminar
April 26, 2022
Nov. 2021
Invited Towards a geometry for syntax
Computer Laboratory, University of Cambridge
November 19, 2021
Nov. 2021
Between abstraction and composition...
Logic and Semantics Seminar, Aarhus University
November 1, 2021
Aug. 2021
Abstraction, composition, and the phase distinction
CMU Speakers Club
August 24, 2021
May 2021
Invited Normalization for Cubical Type Theory
Padova Logic Seminar
Apr. 2021
Invited Logical Relations As Types
CCS Colloquium, Augusta University
Feb. 2021
Normalization for Cubical Type theory
Pittsburgh's HoTT Seminar
Jun. 2020
Invited redtt and the future of Cartesian cubical type theory
Every Proof Assistant
Mar. 2020
Invited Objective Metatheory of Dependent Type Theories
Homotopy Type Theory Electronic Seminar Talks
Jan. 2020
Gluing Models of Type Theory Along Flat Functors
CMU HoTT Seminar
Apr. 2019
Algebraic Type Theory and the Gluing Construction
CMU HoTT Seminar