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

FSCD '22
Sheaf semantics of termination-insensitive noninterference
J. Sterling and R. Harper
International Conference on Formal Structures for Computation and Deduction (FSCD)
doi, abstract, arXiv preprint, local copy, video, slides
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
D. Palombi and J. Sterling
38th International Conference on Mathematical Foundations of Programming Semantics
abstract, arXiv preprint, local copy, slides
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
J. Sterling, C. Angiuli, and D. Gratzer
Logical Methods in Computer Science
doi, abstract, arXiv preprint, local copy
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
Y. Niu, J. Sterling, H. Grodin, and R. Harper
49th ACM SIGPLAN Symposium on Principles of Programming Languages
doi, abstract, external link, arXiv preprint, artifact
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
J. Sterling and C. Angiuli
36th Annual Symposium on Logic in Computer Science
doi, abstract, arXiv preprint, local copy, video, slides
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
J. Sterling
Journal of Functional Programming, Bob Harper Festschrift Collection
doi, abstract, arXiv preprint, artifact
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
J. Sterling and R. Harper
Journal of the ACM
doi, abstract, arXiv preprint, local copy, errata
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
D. Gratzer, J. Sterling, and L. Birkedal
International Conference on Functional Programming (ICFP), 2019
ICFP '19 Distinguished Paper Award
doi, abstract, local copy
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
J. Sterling, C. Angiuli, and D. Gratzer
International Conference on Formal Structures for Computation and Deduction (FSCD)
FSCD '19 Best Paper Award for Junior Researchers
doi, abstract, arXiv preprint, slides
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
J. Sterling and R. Harper
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18)
doi, abstract, arXiv preprint, local copy, slides
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.
doi, abstract
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
Preprint Controlling unfolding in type theory
D. Gratzer, J. Sterling, C. Angiuli, T. Coquand, and L. Birkedal
Under review
abstract, arXiv preprint
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
J. Sterling, D. Gratzer, and L. Birkedal
Under review
abstract, arXiv preprint, local copy
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
J. Sterling
Under review
abstract, arXiv preprint, local copy
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},
}
Jul. 2022
Preprint What should a generic object be?
J. Sterling
Under review
abstract, arXiv preprint, local copy
July 13, 2022
BibTeX citation
@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},
}
Jun. 2022
Preprint Naïve logical relations in synthetic Tait computability
J. Sterling
abstract, local copy
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
D. Gratzer, M. Shulman, and J. Sterling
Under review
doi, abstract, arXiv preprint, local copy
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

Dec. 2022
Invited Controlling unfolding in type theory
J. Sterling
Workshop on Dependent Type Theory (to celebrate the Defense of Loïc Pujet)
abstract, external link
December 14, 2022
MURI '22
Invited Sheaf semantics of termination-insensitive noninterference
J. Sterling and R. Harper
MURI Team Meeting 2022
slides
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
J. Sterling
WG6 kick-off meeting: Syntax and Semantics of Type Theories
abstract, external link
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
J. Sterling
Workshop on the Implementation of Type Systems (keynote)
abstract, external link, video, slides
January 22, 2022
MURI '21
Normalization for (Cartesian) Cubical Type Theory
J. Sterling
MURI Team Meeting 2021
slides
October 15, 2021
ML '21
A metalanguage for multi-phase modularity
J. Sterling and R. Harper
ML Family Workshop 2021
abstract, external link, local copy, video, slides
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
Normalization for cubical type theory
J. Sterling and C. Angiuli
Category Theory 2021
local copy, video, slides
MURI '20
(Cubical) Computability Structures
J. Sterling
MURI Team Meeting 2020
slides
March 2020
HoTT '19
Cubical Exact Equality and Categorical Gluing
J. Sterling, C. Angiuli, and D. Gratzer
International Conference on Homotopy Type Theory, 2019
abstract, slides
TYPES '19
XTT: Cubical Syntax for Extensional Equality (without equality reflection)
J. Sterling, C. Angiuli, and D. Gratzer
TYPES 2019
external link, slides
Aug. 2018
Invited redtt: implementing cartesian cubical type theory
C. Angiuli, E. Cavallo, Favonia, R. Harper, A. Mörtberg, and J. Sterling
Dagstuhl Seminar 18341: Formalization of Mathematics in Type Theory
slides
LFMTP '18
Invited The RedPRL Proof Assistant
C. Angiuli, E. Cavallo, Favonia, R. Harper, and J. Sterling
International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), 2018
doi, abstract
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
J. Sterling
Dissertation Overview, Carnegie Mellon University
local copy
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
J. Sterling
Doctoral Dissertation, Carnegie Mellon University
doi, abstract, external link, local copy, video, slides, errata
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
Notes Practical Semantics
J. Sterling
local copy
October 14, 2022
Feb. 2022
Notes Bilimits in categories of partial maps
J. Sterling
doi, abstract, arXiv preprint, local copy
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
D. Gratzer, M. Shulman, and J. Sterling
doi, abstract, arXiv preprint, local copy, artifact
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
D. Gratzer and J. Sterling
abstract, arXiv preprint
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
J. Sterling and B. Spitters
arXiv preprint
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

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