We show how to construct a logical relation for countable nondeterminism in a guarded type theory, corresponding to the internal logic of the topos Sh ω 1 of sheaves over ω 1. In contrast to earlier work on abstract step-indexed models, we not only construct the logical relations in the guarded type theory, but also give an internal proof of the adequacy of the model with respect to standard contextual equivalence. To state and prove adequacy of the logical relation, we introduce a new propositional modality. In connection with this modality we show why it is necessary to work in the logic of bf Shω 1. © 2014 Springer International Publishing Switzerland.
CITATION STYLE
Bizjak, A., Birkedal, L., & Miculan, M. (2014). A model of countable nondeterminism in guarded type theory. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8560 LNCS, pp. 108–123). Springer Verlag. https://doi.org/10.1007/978-3-319-08918-8_8
Mendeley helps you to discover research relevant for your work.