| WG6 | Invited Naïve logical relations in synthetic Tait computability WG6 kick-off meeting: Syntax and Semantics of Type Theories 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},
} |
| Apr. 2022 | Preprint Classifying topoi in synthetic guarded domain theory: the universal property of multi-clock guarded recursion April 19, 2022 @unpublished{palombi-sterling:2022,
author = {Palombi, Daniele and Sterling, Jonathan},
url = {https://www.jonmsterling.com/papers/palombi-sterling:2022.pdf},
year = {2022},
month = mar,
note = {Unpublished manuscript},
title = {Classifying topoi in synthetic guarded domain theory},
} |
| FSCD '22 | To appear Sheaf semantics of termination-insensitive noninterference International Conference on Formal Structures for Computation and Deduction (FSCD) April 19, 2022 @inproceedings{sterling-harper:2022,
author = {Sterling, Jonathan and Harper, Robert},
editor = {Felty, Amy},
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.15},
eprint = {2204.09421},
eprintclass = {cs.PL},
eprinttype = {arXiv},
number = {15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
title = {Sheaf semantics of termination-insensitive noninterference},
volume = {228},
}
|
| Apr. 2022 | Dissertation Overview: First Steps in Synthetic Tait ComputabilityDissertation Overview, Carnegie Mellon University @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}},
} |
| Feb. 2022 | Preprint Strict universes for Grothendieck topoi Under review 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},
} |
| Feb. 2022 | Notes Bilimits in categories of partial maps 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 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},
} |
| LMCS | A Cubical Language for Bishop Sets Logical Methods in Computer Science 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 49th ACM SIGPLAN Symposium on Principles of Programming Languages 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},
} |
| Sep. 2021 | First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory Doctoral Dissertation, Carnegie Mellon University 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},
} |
| LICS '21 | Normalization for Cubical Type theory 36th Annual Symposium on Logic in Computer Science 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 Journal of Functional Programming, Bob Harper Festschrift Collection 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 Journal of the ACM 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},
}
|
| ML '21 | A metalanguage for multi-phase modularity @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},
}
|
| Dec. 2020 | Notes Syntactic categories for dependent type theory: sketching and adequacy @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},
}
|
| ICFP '19 | Implementing a Modal Dependent Type Theory International Conference on Functional Programming (ICFP), 2019 ICFP '19 Distinguished Paper Award @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 @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},
}
|
| Sep. 2018 | Notes Normalization by gluing for free λ-theories @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},
} |
| LICS '18 | Guarded Computational Type Theory Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18) @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},
}
|
| LFMTP '18 | Invited The RedPRL Proof Assistant International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), 2018 @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)}},
}
|
| LEUS | Invited Dependent Types for Pragmatics 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. @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},
} |