University of Sussex
Browse

File(s) under permanent embargo

A step-indexed Kripke model of hidden state

journal contribution
posted on 2023-06-07, 20:59 authored by Jan Schwinghammer, Lars Birkedal, Francois Pottier, Bernhard ReusBernhard Reus, Kristian Stovring, Hongseok Yang
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.

History

Publication status

  • Published

Journal

Mathematical Structures in Computer Science

ISSN

0960-1295

Publisher

Cambridge University Press

Issue

1

Volume

23

Page range

1-54

Department affiliated with

  • Informatics Publications

Notes

On this one Jan Schwinghammer was main author then the others were all equally involved.

Full text available

  • No

Peer reviewed?

  • Yes

Legacy Posted Date

2013-05-03

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC