Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(14)
Dependent Types
Domain Theory
Indexation
kripke model
Polymorphism
Programming Language
Recursive Types
Reference Model
Semantic Model
Semantics of Programming Languages
Type System
Value Function
Higher Order
Higher Order Logic
Subscribe
Academic
Publications
First Steps in Synthetic Guarded Domain Theory: StepIndexing in the Topos of Trees
First Steps in Synthetic Guarded Domain Theory: StepIndexing in the Topos of Trees,10.1109/LICS.2011.16,Lars Birkedal,Rasmus Ejlers Mogelberg,Jan Sch
Edit
First Steps in Synthetic Guarded Domain Theory: StepIndexing in the Topos of Trees
BibTex

RIS

RefWorks
Download
Lars Birkedal
,
Rasmus Ejlers Mogelberg
,
Jan Schwinghammer
,
Kristian Stovring
We present the topos S of trees as a model of guarded recursion. We study the internal dependentlytyped higherorder 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 stepindexed 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 higherorder store, such as general MLlike 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 manysorted higher order logic extended with modal operators on both types and terms. (Recall that terms in higherorder 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 theSlogic, we present a model of F; ref , a callbyvalue
programming language
with impredicative polymorphism, recursive types, and general MLlike refer ences.
Conference:
Logic in Computer Science  LICS
, pp. 5564, 2011
DOI:
10.1109/LICS.2011.16
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.
(
ieeexplore.ieee.org
)
(
ieeexplore.ieee.org
)
References
(24)
Representing Nested Inductive Types using {Wtypes
(
Citations: 8
)
Michael Abbott
,
Thorsten Altenkirch
,
Neil Ghani
Published in 2004.
Statedependent representation independence
(
Citations: 41
)
Amal Ahmed
,
Derek Dreyer
,
Andreas Rossberg
Conference:
ACM SIGPLANSIGACT Symposium on Principles of Programming Languages  POPL
, pp. 340353, 2009
A very modal model of a modern, major, general type system
(
Citations: 37
)
Andrew W. Appel
,
Paulandré Melliès
,
Christopher D. Richards
,
Jérôme Vouillon
Conference:
ACM SIGPLANSIGACT Symposium on Principles of Programming Languages  POPL
, pp. 109122, 2007
Stepindexed kripke models over recursive worlds
(
Citations: 2
)
Lars Birkedal
,
Bernhard Reus
,
Jan Schwinghammer
,
Kristian Støvring
,
Jacob Thamsborg
,
Hongseok Yang
Journal:
Sigplan Notices  SIGPLAN
, pp. 119132, 2011
A StepIndexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces
(
Citations: 1
)
Jan Schwinghammer
,
Lars Birkedal
,
Kristian Støvring
Conference:
Foundations of Software Science and Computation Structure  FoSSaCS
, pp. 305319, 2011