Step-indexed Kripke models over recursive worlds

TY - GEN

T1 - Step-indexed Kripke models over recursive worlds

AU - Birkedal, Lars

AU - Reus, Bernhard

AU - Schwinghammer, Jan

AU - Støvring, Kristian

AU - Thamsborg, Jacob

AU - Yang, Hongseok

N1 - Conference code: 38

PY - 2011/1

Y1 - 2011/1

N2 - Over the last decade, there has been extensive research on modelling challenging features in programming languages and program logics, such as higher-order store and storable resource invariants. A recent line of work has identified a common solution to some of these challenges: Kripke models over worlds that are recursively defined in a category of metric spaces. In this paper, we broaden the scope of this technique from the original domain-theoretic setting to an elementary, operational one based on step indexing. The resulting method is widely applicable and leads to simple, succinct models of complicated language features, as we demonstrate in our semantics of Charguéraud and Pottier's type-and-capability system for an ML-like higher-order language. Moreover, the method provides a high-level understanding of the essence of recent approaches based on step indexing.

AB - Over the last decade, there has been extensive research on modelling challenging features in programming languages and program logics, such as higher-order store and storable resource invariants. A recent line of work has identified a common solution to some of these challenges: Kripke models over worlds that are recursively defined in a category of metric spaces. In this paper, we broaden the scope of this technique from the original domain-theoretic setting to an elementary, operational one based on step indexing. The resulting method is widely applicable and leads to simple, succinct models of complicated language features, as we demonstrate in our semantics of Charguéraud and Pottier's type-and-capability system for an ML-like higher-order language. Moreover, the method provides a high-level understanding of the essence of recent approaches based on step indexing.

U2 - 10.1145/1925844.1926401

DO - 10.1145/1925844.1926401

M3 - Conference article

SN - 1523-2867

VL - 46

SP - 119

EP - 131

JO - SIGPLAN Notices (ACM Special Interest Group on Programming Languages)

JF - SIGPLAN Notices (ACM Special Interest Group on Programming Languages)

IS - 1

T2 - 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Y2 - 26 January 2011 through 28 January 2011

ER -