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

Jan Schwinghammer; Lars Birkedal; Kristian Støvring

doi:10.1007/978-3-642-19805-2_21

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

Jan Schwinghammer, Lars Birkedal, Kristian Støvring

Department of Computer Science

5 Citations (Scopus)

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 the first sound model for Charguéraud and Pottier's type and capability system including both frame and anti-frame rules. The model is a possible worlds model based on the operational semantics and step-indexed heap relations, and the worlds are constructed as a recursively defined predicate on a recursively defined metric space. We also extend the model to account for Pottier's generalized frame and anti-frame rules, where invariants are generalized to families of invariants indexed over pre-orders. This generalization enables reasoning about some well-bracketed as well as (locally) monotonic uses of local state.

Original language	English
Title of host publication	Foundations of Software Science and Computational Structures : 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26–April 3, 2011. Proceedings
Editors	Martin Hofman
Number of pages	15
Publisher	Springer
Publication date	2011
Pages	305-319
ISBN (Print)	978-3-642-19804-5
ISBN (Electronic)	978-3-642-19805-2
DOIs	https://doi.org/10.1007/978-3-642-19805-2_21
Publication status	Published - 2011
Event	14th International Conference on Foundations of Software Science and Computational Structures - Saarbrücken, Germany Duration: 26 Mar 2011 → 3 Apr 2011 Conference number: 14

Conference

Conference	14th International Conference on Foundations of Software Science and Computational Structures
Number	14
Country/Territory	Germany
City	Saarbrücken
Period	26/03/2011 → 03/04/2011

Series	Lecture notes in computer science
Volume	6604
ISSN	0302-9743

Access to Document

10.1007/978-3-642-19805-2_21

10.1007%2F978-3-642-19805-2_21.pdfFinal published version, 280 KB

Cite this

Schwinghammer, J., Birkedal, L., & Støvring, K. (2011). A step-indexed Kripke model of hidden state via recursive properties on recursively defined metric spaces. In M. Hofman (Ed.), Foundations of Software Science and Computational Structures: 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26–April 3, 2011. Proceedings (pp. 305-319). Springer. Lecture notes in computer science Vol. 6604 https://doi.org/10.1007/978-3-642-19805-2_21

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

Foundations of Software Science and Computational Structures: 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26–April 3, 2011. Proceedings. ed. / Martin Hofman. Springer, 2011. p. 305-319 (Lecture notes in computer science, Vol. 6604).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Schwinghammer, J, Birkedal, L & Støvring, K 2011, A step-indexed Kripke model of hidden state via recursive properties on recursively defined metric spaces. in M Hofman (ed.), Foundations of Software Science and Computational Structures: 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26–April 3, 2011. Proceedings. Springer, Lecture notes in computer science, vol. 6604, pp. 305-319, 14th International Conference on Foundations of Software Science and Computational Structures, Saarbrücken, Germany, 26/03/2011. https://doi.org/10.1007/978-3-642-19805-2_21

Schwinghammer J, Birkedal L, Støvring K. A step-indexed Kripke model of hidden state via recursive properties on recursively defined metric spaces. In Hofman M, editor, Foundations of Software Science and Computational Structures: 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26–April 3, 2011. Proceedings. Springer. 2011. p. 305-319. (Lecture notes in computer science, Vol. 6604). doi: 10.1007/978-3-642-19805-2_21

Schwinghammer, Jan ; Birkedal, Lars ; Støvring, Kristian. / A step-indexed Kripke model of hidden state via recursive properties on recursively defined metric spaces. Foundations of Software Science and Computational Structures: 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26–April 3, 2011. Proceedings. editor / Martin Hofman. Springer, 2011. pp. 305-319 (Lecture notes in computer science, Vol. 6604).

@inproceedings{7915467123fb420e9c9e14f0e85296d2,

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 the first sound model for Chargu{\'e}raud and Pottier's type and capability system including both frame and anti-frame rules. The model is a possible worlds model based on the operational semantics and step-indexed heap relations, and the worlds are constructed as a recursively defined predicate on a recursively defined metric space. We also extend the model to account for Pottier's generalized frame and anti-frame rules, where invariants are generalized to families of invariants indexed over pre-orders. This generalization enables reasoning about some well-bracketed as well as (locally) monotonic uses of local state.",

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

year = "2011",

doi = "10.1007/978-3-642-19805-2_21",

language = "English",

isbn = "978-3-642-19804-5",

series = "Lecture notes in computer science",

publisher = "Springer",

pages = "305--319",

editor = "Martin Hofman",

booktitle = "Foundations of Software Science and Computational Structures",

note = "14th International Conference on Foundations of Software Science and Computational Structures ; Conference date: 26-03-2011 Through 03-04-2011",

}

TY - GEN

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

AU - Schwinghammer, Jan

AU - Birkedal, Lars

AU - Støvring, Kristian

N1 - Conference code: 14

PY - 2011

Y1 - 2011

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 the first sound model for Charguéraud and Pottier's type and capability system including both frame and anti-frame rules. The model is a possible worlds model based on the operational semantics and step-indexed heap relations, and the worlds are constructed as a recursively defined predicate on a recursively defined metric space. We also extend the model to account for Pottier's generalized frame and anti-frame rules, where invariants are generalized to families of invariants indexed over pre-orders. This generalization enables reasoning about some well-bracketed as well as (locally) monotonic uses of local state.

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 the first sound model for Charguéraud and Pottier's type and capability system including both frame and anti-frame rules. The model is a possible worlds model based on the operational semantics and step-indexed heap relations, and the worlds are constructed as a recursively defined predicate on a recursively defined metric space. We also extend the model to account for Pottier's generalized frame and anti-frame rules, where invariants are generalized to families of invariants indexed over pre-orders. This generalization enables reasoning about some well-bracketed as well as (locally) monotonic uses of local state.

U2 - 10.1007/978-3-642-19805-2_21

DO - 10.1007/978-3-642-19805-2_21

M3 - Article in proceedings

SN - 978-3-642-19804-5

T3 - Lecture notes in computer science

SP - 305

EP - 319

BT - Foundations of Software Science and Computational Structures

A2 - Hofman, Martin

PB - Springer

T2 - 14th International Conference on Foundations of Software Science and Computational Structures

Y2 - 26 March 2011 through 3 April 2011

ER -

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

Abstract

Conference

Access to Document

Fingerprint

Cite this