A step-indexed Kripke model of hidden state via recursive properties on recursively defined metric spaces

Lars Birkedal; Jan Schwinghammer; Kristian Støvring

A step-indexed Kripke model of hidden state via recursive properties on recursively defined metric spaces

Lars Birkedal, Jan Schwinghammer, Kristian Støvring

Datalogisk Institut

Abstract

Frame and anti-frame rules have been proposed as proof rules for modular reasoning about programs. Frame rules allow one to hide irrelevant parts of the state during verification, whereas the anti-frame rule allows one to hide local state from the context. We give a possible worlds semantics for Chargu´eraud and Pottier’s type and capability system including frame and anti-frame rules,
based on the operational semantics and step-indexed heap relations. The worlds are constructed as a recursively defined predicate on a recursively defined metric space, which provides a considerably simpler alternative compared to a previous construction.

Originalsprog	Engelsk
Titel	7th Workshop on Fixed Points in Computer Science, FICS 2010
Redaktører	Luigi Santocanale
Antal sider	7
Publikationsdato	2010
Sider	27-33
Status	Udgivet - 2010
Begivenhed	7th Workshop on Fixed Points in Computer Science - Brno, Tjekkiet Varighed: 21 aug. 2010 → 22 aug. 2010 Konferencens nummer: 7

Konference

Konference	7th Workshop on Fixed Points in Computer Science
Nummer	7
Land/Område	Tjekkiet
By	Brno
Periode	21/08/2010 → 22/08/2010

Adgang til dokumentet

https://hal.archives-ouvertes.fr/hal-00512377

Citationsformater

A step-indexed Kripke model of hidden state via recursive properties on recursively defined metric spaces. / Birkedal, Lars; Schwinghammer, Jan; Støvring, Kristian.

7th Workshop on Fixed Points in Computer Science, FICS 2010. red. / Luigi Santocanale. 2010. s. 27-33.

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

Birkedal, L, Schwinghammer, J & Støvring, K 2010, A step-indexed Kripke model of hidden state via recursive properties on recursively defined metric spaces. i L Santocanale (red.), 7th Workshop on Fixed Points in Computer Science, FICS 2010. s. 27-33, 7th Workshop on Fixed Points in Computer Science, Brno, Tjekkiet, 21/08/2010. <https://hal.archives-ouvertes.fr/hal-00512377>

@inproceedings{512e77d359a248bc99f11c8d9856a2a8,

title = "A step-indexed Kripke model of hidden state via recursive properties on recursively defined metric spaces",

abstract = "Frame and anti-frame rules have been proposed as proof rules for modular reasoning about programs. Frame rules allow one to hide irrelevant parts of the state during verification, whereas the anti-frame rule allows one to hide local state from the context. We give a possible worlds semantics for Chargu´eraud and Pottier{\textquoteright}s type and capability system including frame and anti-frame rules,based on the operational semantics and step-indexed heap relations. The worlds are constructed as a recursively defined predicate on a recursively defined metric space, which provides a considerably simpler alternative compared to a previous construction.",

author = "Lars Birkedal and Jan Schwinghammer and Kristian St{\o}vring",

year = "2010",

language = "English",

pages = "27--33",

editor = "Luigi Santocanale",

booktitle = "7th Workshop on Fixed Points in Computer Science, FICS 2010",

note = "7th Workshop on Fixed Points in Computer Science ; Conference date: 21-08-2010 Through 22-08-2010",

}

TY - GEN

T1 - A step-indexed Kripke model of hidden state via recursive properties on recursively defined metric spaces

AU - Birkedal, Lars

AU - Schwinghammer, Jan

AU - Støvring, Kristian

N1 - Conference code: 7

PY - 2010

Y1 - 2010

N2 - Frame and anti-frame rules have been proposed as proof rules for modular reasoning about programs. Frame rules allow one to hide irrelevant parts of the state during verification, whereas the anti-frame rule allows one to hide local state from the context. We give a possible worlds semantics for Chargu´eraud and Pottier’s type and capability system including frame and anti-frame rules,based on the operational semantics and step-indexed heap relations. The worlds are constructed as a recursively defined predicate on a recursively defined metric space, which provides a considerably simpler alternative compared to a previous construction.

AB - Frame and anti-frame rules have been proposed as proof rules for modular reasoning about programs. Frame rules allow one to hide irrelevant parts of the state during verification, whereas the anti-frame rule allows one to hide local state from the context. We give a possible worlds semantics for Chargu´eraud and Pottier’s type and capability system including frame and anti-frame rules,based on the operational semantics and step-indexed heap relations. The worlds are constructed as a recursively defined predicate on a recursively defined metric space, which provides a considerably simpler alternative compared to a previous construction.

M3 - Article in proceedings

SP - 27

EP - 33

BT - 7th Workshop on Fixed Points in Computer Science, FICS 2010

A2 - Santocanale, Luigi

T2 - 7th Workshop on Fixed Points in Computer Science

Y2 - 21 August 2010 through 22 August 2010

ER -