A step-indexed Kripke Model of Hidden State

Jan Schwinghammer (1) , Lars Birkedal (2) , François Pottier (3) , Bernhard Reus (4) , Kristian Støvring (5) , Hongseok Yang (6)

1 Programming Systems Lab [Saarland]
2 ITU - IT University of Copenhagen
3 GALLIUM - Programming languages, types, compilation and proofs
4 Department of Informatics [Brighton]
5 DIKU - Department of Computer Science [Copenhagen]
6 OUCL - Computing Laboratory

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.

Domaines: Langage de programmation [cs.PL]

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, 2013, 23 (1), pp.1--54. ⟨hal-00772757⟩