| POPL '22 | 49th ACM SIGPLAN Symposium on Principles of Programming Languages @unpublished{niu-sterling-grodin-harper:2021,
author = {Niu, Yue and Sterling, Jonathan and Grodin, Harrison and Harper, Robert},
year = {2021},
eprint = {2107.04663},
eprintclass = {cs.PL},
eprinttype = {arXiv},
note = {To appear in POPL '22},
title = {A cost-aware logical framework},
}
|
| Sep. 13, '21 | Carnegie Mellon University @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 | 36th Annual Symposium on Logic in Computer Science @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 | Journal of Functional Programming, Bob Harper Festschrift Collection @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 | Journal of the ACM @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 | @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. '20 | @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},
}
|
| Feb. '20 | @unpublished{sterling-angiuli-gratzer:2020,
author = {Sterling, Jonathan and Angiuli, Carlo and Gratzer, Daniel},
year = {2020},
eprint = {2003.01491},
eprintclass = {cs.LO},
eprinttype = {arXiv},
note = {Under review},
title = {A cubical language for {Bishop} sets},
}
|
| ICFP '19 | 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 | International Conference on Formal Structures for Computation and Deduction (FSCD), 2019 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},
}
|
| LFMTP '18 | 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)}},
}
|
| LICS '18 | 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},
}
|
| LEUS | 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{mcadams-sterling:2016,
author={McAdams, Darryl 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},
url={https://doi.org/10.1007/978-3-319-26506-3_4}
}
|