DocumentCode :
2545182
Title :
First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees
Author :
Birkedal, Lars ; Møgelberg, Rasmus Ejlers ; Schwinghammer, Jan ; Støvring, Kristian
Author_Institution :
IT Univ. of Copenhagen, Copenhagen, Denmark
fYear :
2011
fDate :
21-24 June 2011
Firstpage :
55
Lastpage :
64
Abstract :
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.
Keywords :
formal logic; programming languages; trees (mathematics); guarded recursion; internal dependently-typed higher-order logic; modal operators; program logics; programming languages; step-indexing; synthetic guarded domain theory; topos of trees; Algebra; Cognition; Computational modeling; Computer languages; Equations; Mathematical model; Semantics; domain theory; logic; semantics; step-indexing;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Logic in Computer Science (LICS), 2011 26th Annual IEEE Symposium on
Conference_Location :
Toronto, ON
ISSN :
1043-6871
Print_ISBN :
978-1-4577-0451-2
Electronic_ISBN :
1043-6871
Type :
conf
DOI :
10.1109/LICS.2011.16
Filename :
5970227
Link To Document :
بازگشت