Bibliography

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

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

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

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

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

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

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