Bibliography of Jonathan Sterling

Table of contents

The following authors are represented in this bibliography: Carlo Angiuli, Lars Birkedal, Evan Cavallo, Daniel Gratzer, Harrison Grodin, Robert Harper, Favonia, 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, citation
June 28, 2022
@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, local copy, slides, citation
April 19, 2022
@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, citation
February 9, 2022
@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, citation
January 2022
@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, citation
July 7, 2021
@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, citation
May 19, 2021
@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, citation, errata
May 2021
@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, 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, 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, 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, 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

Jul. 2022
Preprint What should a generic object be?
J. Sterling
Under review
abstract, local copy, citation
July 13, 2022
@unpublished{sterling:2022:generic,
  author = {Sterling, Jonathan},
  year = {2022},
  month = jul,
  note = {Unpublished manuscript},
  title = {What should a generic object be?},
}
Jul. 2022
Preprint Denotational semantics of general store and polymorphism
J. Sterling, D. Gratzer, and L. Birkedal
abstract, local copy, 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},
}
Jun. 2022
Preprint Naïve logical relations in synthetic Tait computability
J. Sterling
abstract, local copy, 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, citation
February 21, 2022
@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},
}
Dec. 2020
Preprint Syntactic categories for dependent type theory: sketching and adequacy
D. Gratzer and J. Sterling
abstract, arXiv preprint, 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},
}

Workshop Presentations

MURI '22
Invited Sheaf semantics of termination-insensitive noninterference
J. Sterling and R. Harper
MURI Team Meeting 2022
slides, citation
June 30, 2022
@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, citation
May 20, 2022
@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},
}
ML '21
A metalanguage for multi-phase modularity
J. Sterling and R. Harper
ML Family Workshop 2021
abstract, external link, local copy, video, slides, 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},
}
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, 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, 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, citation, errata
September 13, 2021
@phdthesis{sterling:2021:thesis,
  author = {Sterling, Jonathan},
  school = {Carnegie Mellon University},
  year = {2021},
  doi = {10.5281/zenodo.5709838},
  note = {CMU technical report 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
J. Sterling
doi, abstract, arXiv preprint, local copy, citation
February 17, 2022
@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, citation
February 15, 2022
@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},
}
Sep. 2018
Notes Normalization by gluing for free λ-theories
J. Sterling and B. Spitters
arXiv preprint, 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},
}