First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees

First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees,10.1109/LICS.2011.16,Lars Birkedal,Rasmus Ejlers Mogelberg,Jan Sch

First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees  
BibTex | RIS | RefWorks Download
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. I. INTRODUCTION Recursive definitions are ubiquitous in computer science. In particular, in semantics of programming languages and program logics we often use recursively defined functions and relations, and also recursively defined types (domains). For example, in recent years there has been extensive work on giving semantics of type systems for programming lan- guages with dynamically allocated higher-order store, such as general ML-like references. Models have been expressed as Kripke models over a recursively defined set of worlds (an example of a recursively defined domain) and have involved recursively defined relations to interpret the recursive types of the programming language; see (4) and the references therein. In this paper we study a toposS, which we show models guarded recursion in the sense that it allows for guarded recursive definitions of both recursive functions and relations as well as recursive types. The toposS is known as the topos of trees (or forests); what is new here is our application of this topos to model guarded recursion. The internal logic ofS is a standard many-sorted higher- order logic extended with modal operators on both types and terms. (Recall that terms in higher-order logic include both functions and relations, as the latter are simply Prop- valued functions.) This internal logic can then be used as a language to describe semantic models of programming languages with the features mentioned above. As an example which uses both recursively defined types and recursively defined relations in theS-logic, we present a model of F; ref , a call-by-value programming language with impredicative polymorphism, recursive types, and general ML-like refer- ences.
Conference: Logic in Computer Science - LICS , pp. 55-64, 2011
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.