Bibliography

• Normalization for Cubical Type Theory
  36th Annual Symposium on Logic in Computer Science.
  J. Sterling, C. Angiuli.

  @inproceedings{sterling-angiuli:2021,
    author = {Sterling, Jonathan and Angiuli, Carlo},
    title = {Normalization for Cubical Type Theory},
    booktitle = {Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science},
    series = {LICS '21},
    year = {2021},
    publisher = {ACM},
    address = {New York, NY, USA},
    note = {To appear},
    eprint = {2101.11479},
    eprintclass = {cs.LO},
    eprinttype = {arXiv},
  }
          

• Implementing a Modal Dependent Type Theory.
  D. Gratzer, J. Sterling, and L. Birkedal.
  International Conference on Functional Programming (ICFP), 2019.

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

• Cubical Syntax for Reflection-Free Extensional Equality.
  J. Sterling, C. Angiuli, and D. Gratzer.
  International Conference on Formal Structures for Computation and Deduction (FSCD), 2019.

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

• The RedPRL Proof Assistant.
  C. Angiuli, E. Cavallo, K. Hou (Favonia), R. Harper, and J. Sterling.
  (Invited Paper)
  International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), 2018.

  @inproceedings{redprl:lfmtp:2018,
    author    = {Angiuli, Carlo and Cavallo, Evan and Hou (Favonia), Kuen-Bang and Harper, Robert and Sterling, Jonathan},
    year      = {2018},
    title     = {The RedPRL Proof Assistant (Invited Paper)},
    editor    = {Blanqui, Fr\'ed\'eric and Reis, Giselle},
    booktitle = {{\rm Proceedings of the 13th International Workshop on}
                 Logical Frameworks and Meta-Languages: Theory and Practice,
                 {\rm Oxford, UK, 7th July 2018}},
    series    = {Electronic Proceedings in Theoretical Computer Science},
    volume    = {274},
    publisher = {Open Publishing Association},
    pages     = {1-10},
    doi       = {10.4204/EPTCS.274.1},
  }
          

• Guarded Computational Type Theory.
  J. Sterling, R. Harper.
  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},
  }
          

• Dependent Types for Pragmatics.
  D. McAdams, J. Sterling.
  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}
  }