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

Department of Computer Science

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.

Original language	English
Title of host publication	7th Workshop on Fixed Points in Computer Science, FICS 2010
Editors	Luigi Santocanale
Number of pages	7
Publication date	2010
Pages	27-33
Publication status	Published - 2010
Event	7th Workshop on Fixed Points in Computer Science - Brno, Czech Republic Duration: 21 Aug 2010 → 22 Aug 2010 Conference number: 7

Conference

Conference	7th Workshop on Fixed Points in Computer Science
Number	7
Country/Territory	Czech Republic
City	Brno
Period	21/08/2010 → 22/08/2010

Access to Document

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

Cite this

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. ed. / Luigi Santocanale. 2010. p. 27-33.

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › 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. in L Santocanale (ed.), 7th Workshop on Fixed Points in Computer Science, FICS 2010. pp. 27-33, 7th Workshop on Fixed Points in Computer Science, Brno, Czech Republic, 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 -