A step-indexed Kripke model of hidden state

Jan Schwinghammer; Lars Birkedal; François Pottier; Bernhard Reus; Kristian Støvring; Hongseok Yang

doi:10.1017/S0960129512000035

A step-indexed Kripke model of hidden state

Jan Schwinghammer, Lars Birkedal, François Pottier, Bernhard Reus, Kristian Støvring, Hongseok Yang

Datalogisk Institut

4 Citationer (Scopus)

Abstract

Frame and anti-frame rules have been proposed as proof rules for modular reasoning about programs. Frame rules allow the hiding of irrelevant parts of the state during verification, whereas the anti-frame rule allows the hiding of local state from the context. We discuss the semantic foundations of frame and anti-frame rules, and present the first sound model for Charguéraud and Pottier's type and capability system including both of these rules. The model is a possible worlds model based on the operational semantics and step-indexed heap relations, and the worlds are given by a recursively defined metric space. We also extend the model to account for Pottier's generalised frame and anti-frame rules, where invariants are generalised to families of invariants indexed over preorders. This generalisation enables reasoning about some well-bracketed as well as (locally) monotone uses of local state.

Originalsprog	Engelsk
Tidsskrift	Mathematical Structures in Computer Science
Vol/bind	23
Udgave nummer	1
Sider (fra-til)	1-54
Antal sider	54
ISSN	0960-1295
DOI	https://doi.org/10.1017/S0960129512000035
Status	Udgivet - feb. 2013

Adgang til dokumentet

10.1017/S0960129512000035

Citationsformater

@article{797aea4a596f4955bc2513b261694698,

title = "A step-indexed Kripke model of hidden state",

abstract = "Frame and anti-frame rules have been proposed as proof rules for modular reasoning about programs. Frame rules allow the hiding of irrelevant parts of the state during verification, whereas the anti-frame rule allows the hiding of local state from the context. We discuss the semantic foundations of frame and anti-frame rules, and present the first sound model for Chargu{\'e}raud and Pottier's type and capability system including both of these rules. The model is a possible worlds model based on the operational semantics and step-indexed heap relations, and the worlds are given by a recursively defined metric space. We also extend the model to account for Pottier's generalised frame and anti-frame rules, where invariants are generalised to families of invariants indexed over preorders. This generalisation enables reasoning about some well-bracketed as well as (locally) monotone uses of local state.",

author = "Jan Schwinghammer and Lars Birkedal and Fran{\c c}ois Pottier and Bernhard Reus and Kristian St{\o}vring and Hongseok Yang",

year = "2013",

month = feb,

doi = "10.1017/S0960129512000035",

language = "English",

volume = "23",

pages = "1--54",

journal = "Mathematical Structures in Computer Science",

issn = "0960-1295",

publisher = "Cambridge University Press",

number = "1",

}

TY - JOUR

T1 - A step-indexed Kripke model of hidden state

AU - Schwinghammer, Jan

AU - Birkedal, Lars

AU - Pottier, François

AU - Reus, Bernhard

AU - Støvring, Kristian

AU - Yang, Hongseok

PY - 2013/2

Y1 - 2013/2

N2 - Frame and anti-frame rules have been proposed as proof rules for modular reasoning about programs. Frame rules allow the hiding of irrelevant parts of the state during verification, whereas the anti-frame rule allows the hiding of local state from the context. We discuss the semantic foundations of frame and anti-frame rules, and present the first sound model for Charguéraud and Pottier's type and capability system including both of these rules. The model is a possible worlds model based on the operational semantics and step-indexed heap relations, and the worlds are given by a recursively defined metric space. We also extend the model to account for Pottier's generalised frame and anti-frame rules, where invariants are generalised to families of invariants indexed over preorders. This generalisation enables reasoning about some well-bracketed as well as (locally) monotone uses of local state.

AB - Frame and anti-frame rules have been proposed as proof rules for modular reasoning about programs. Frame rules allow the hiding of irrelevant parts of the state during verification, whereas the anti-frame rule allows the hiding of local state from the context. We discuss the semantic foundations of frame and anti-frame rules, and present the first sound model for Charguéraud and Pottier's type and capability system including both of these rules. The model is a possible worlds model based on the operational semantics and step-indexed heap relations, and the worlds are given by a recursively defined metric space. We also extend the model to account for Pottier's generalised frame and anti-frame rules, where invariants are generalised to families of invariants indexed over preorders. This generalisation enables reasoning about some well-bracketed as well as (locally) monotone uses of local state.

U2 - 10.1017/S0960129512000035

DO - 10.1017/S0960129512000035

M3 - Journal article

SN - 0960-1295

VL - 23

SP - 1

EP - 54

JO - Mathematical Structures in Computer Science

JF - Mathematical Structures in Computer Science

IS - 1

ER -

A step-indexed Kripke model of hidden state

Abstract

Adgang til dokumentet

Fingeraftryk

Citationsformater