Loading...
Please wait, while we are loading the content...
Similar Documents
First steps in synthetic guarded domain theory: Step-indexing in the topos of trees (2011)
| Content Provider | CiteSeerX |
|---|---|
| Author | Støvring, Kristian Birkedal, Lars Møgelberg, Rasmus Ejlers Schwinghammer, Jan |
| Abstract | 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. 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 wellfounded basis, the topos of sheaves over A forms a model of synthetic guarded domain theory, generalizing the results for S. 1. |
| File Format | |
| Publisher Date | 2011-01-01 |
| Publisher Institution | In Proc. of LICS |
| Access Restriction | Open |
| Subject Keyword | Dependent Type Right Setting Domain Theory Complete Heyting Algebra Guarded Recursion Higher-order Store Recursive Definition Modal Operator First Step Internal Logic Recursive Type Equation Step-indexed Model Recursive Type Internal Dependently-typed Higher-order Logic Synthetic Construction Abstract Version Wellfounded Basis Program Logic Axiomatic Categorical Treatment Programming Language |
| Content Type | Text |
| Resource Type | Article |
