
J. Sterling, C. Angiuli, and D. Gratzer
Cubical Syntax for ReflectionFree Extensional Equality
(To Appear)
International Conference on Formal Structures for Computation and Deduction (FSCD), 2019
@unpublished{sterlingangiuligratzer:2019:arxiv,
author = {Sterling, Jonathan and Angiuli, Carlo and Gratzer, Daniel},
url = {https://arxiv.org/abs/1904.08562},
year = {2019},
eprint = {1904.08562},
eprinttype = {arXiv},
note = {Extended version, accepted to FSCD 2019},
title = {Cubical Syntax for ReflectionFree Extensional Equality},
}

C. Angiuli, E. Cavallo, K. Hou (Favonia), R. Harper, and J. Sterling
The RedPRL Proof Assistant
(Invited Paper)
International Workshop on Logical Frameworks and MetaLanguages: Theory and Practice (LFMTP), 2018
@inproceedings{redprl:lfmtp:2018,
author = {Angiuli, Carlo and Cavallo, Evan and Hou (Favonia), KuenBang 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 MetaLanguages: Theory and Practice,
{\rm Oxford, UK, 7th July 2018}},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = {274},
publisher = {Open Publishing Association},
pages = {110},
doi = {10.4204/EPTCS.274.1},
}

J. Sterling, R. Harper
Guarded Computational Type Theory
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18)
@inproceedings{sterlingharper: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 = {9781450355834},
location = {Oxford, United Kingdom},
pages = {879888},
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},
}

D. McAdams, J. Sterling
Dependent Types for Pragmatics
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{mcadamssterling: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={123139},
isbn={9783319265063},
doi={10.1007/9783319265063_4},
url={https://doi.org/10.1007/9783319265063_4}
}