HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Journal articles

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 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 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 generalized frame and anti-frame rules, where invariants are generalized to families of invariants indexed over preorders. This generalization enables reasoning about some well-bracketed as well as (locally) monotone uses of local state.
Document type :
Journal articles
Complete list of metadata

Cited literature [34 references]  Display  Hide  Download

Contributor : François Pottier Connect in order to contact the contributor
Submitted on : Friday, January 11, 2013 - 10:10:25 AM
Last modification on : Thursday, February 3, 2022 - 11:16:57 AM
Long-term archiving on: : Friday, April 12, 2013 - 11:20:23 AM


Files produced by the author(s)


  • HAL Id : hal-00772757, version 1



Jan Schwinghammer, Lars Birkedal, François Pottier, Bernhard Reus, Kristian Støvring, et al.. A step-indexed Kripke Model of Hidden State. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2013, 23 (1), pp.1--54. ⟨hal-00772757⟩



Record views


Files downloads