# Publication details

##
First steps in synthetic guarded domain theory: step-indexing in the topos of trees

Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, Kristian Støvring

Logical Methods in Computer Science, 2012

We present the topos S of trees as a model of guarded
recursion. We study the internal dependently-typed higher-order
logic of S and show that S models two modal
operators, on predicates and types, which serve as guards in recursive
definitions of terms, predicates, and types. In particular, we show how to solve
recursive type equations involving dependent types. We
propose that the internal logic of S provides the right
setting for the synthetic construction of abstract versions of
step-indexed models of programming languages and program logics. As
an example, we show how to construct a model of a programming
language with higher-order store and recursive types entirely inside
the internal logic of S.
Moreover, we give an axiomatic categorical treatment of models
of synthetic guarded domain theory and prove that, for any
complete Heyting algebra A with a well-founded basis,
the topos of sheaves over A forms a model
of synthetic guarded domain theory, generalizing the
results for S.

*This is an expanded and revised version of a paper that
appeared at LICS'11. In addition to
containing more examples and proofs, it also contains a more general
treatment of models of synthetic guarded domain theory.*

Download PDF
Show BibTeX

@ARTICLE{BirkedalEtAl:2011:First:0,
title = {First steps in synthetic guarded domain theory: step-indexing in the topos of trees},
author = {Lars Birkedal and Rasmus Ejlers Møgelberg and Jan Schwinghammer and Kristian Støvring},
year = {2012},
journal = {Logical Methods in Computer Science},
note = {To appear},
}

Login to edit

Legal notice, Privacy policy