A step-indexed Kripke model of hidden state

Schwinghammer, Jan, Birkedal, Lars, Pottier, Francois, Reus, Bernhard, Stovring, Kristian and Yang, Hongseok (2012) A step-indexed Kripke model of hidden state. Mathematical Structures in Computer Science, 23 (1). pp. 1-54. ISSN 0960-1295

[img] PDF
Restricted to SRO admin only

Download (568kB)


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 Chargueraud 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.

Item Type: Article
Additional Information: On this one Jan Schwinghammer was main author then the others were all equally involved.
Schools and Departments: School of Engineering and Informatics > Informatics
Depositing User: Bernhard Reus
Date Deposited: 03 May 2013 11:24
Last Modified: 01 Jul 2019 13:30
URI: http://sro.sussex.ac.uk/id/eprint/17794

View download statistics for this item

📧 Request an update