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

Datalogisk Institut

5 Citationer (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.

Originalsprog	Engelsk
Titel	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
Redaktører	Martin Hofman
Antal sider	15
Forlag	Springer
Publikationsdato	2011
Sider	305-319
ISBN (Trykt)	978-3-642-19804-5
ISBN (Elektronisk)	978-3-642-19805-2
DOI	https://doi.org/10.1007/978-3-642-19805-2_21
Status	Udgivet - 2011
Begivenhed	14th International Conference on Foundations of Software Science and Computational Structures - Saarbrücken, Tyskland Varighed: 26 mar. 2011 → 3 apr. 2011 Konferencens nummer: 14

Konference

Konference	14th International Conference on Foundations of Software Science and Computational Structures
Nummer	14
Land/Område	Tyskland
By	Saarbrücken
Periode	26/03/2011 → 03/04/2011

Navn	Lecture notes in computer science
Vol/bind	6604
ISSN	0302-9743

Adgang til dokumentet

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

10.1007%2F978-3-642-19805-2_21.pdfForlagets udgivne version, 280 KB

Citationsformater

Schwinghammer, J., Birkedal, L., & Støvring, K. (2011). A step-indexed Kripke model of hidden state via recursive properties on recursively defined metric spaces. I M. Hofman (red.), 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 (s. 305-319). Springer. Lecture notes in computer science Bind 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. red. / Martin Hofman. Springer, 2011. s. 305-319 (Lecture notes in computer science, Bind 6604).

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › 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. i M Hofman (red.), 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, bind 6604, s. 305-319, 14th International Conference on Foundations of Software Science and Computational Structures, Saarbrücken, Tyskland, 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. I Hofman M, red., 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. s. 305-319. (Lecture notes in computer science, Bind 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. red. / Martin Hofman. Springer, 2011. s. 305-319 (Lecture notes in computer science, Bind 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

Konference

Adgang til dokumentet

Fingeraftryk

Citationsformater