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 IT University of Copenhagen
3 GALLIUM - Programming languages, types, compilation and proofs
Inria Paris-Rocquencourt
4 Department of Informatics
5 DIKU - Department of computer Science [Copenhagen]
6 OUCL - Computing Laboratory
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.
Type de document :
Article dans une revue
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2013, 23 (1), pp.1--54
Liste complète des métadonnées

Littérature citée [34 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-00772757
Contributeur : François Pottier <>
Soumis le : vendredi 11 janvier 2013 - 10:10:25
Dernière modification le : vendredi 25 mai 2018 - 12:02:07
Document(s) archivé(s) le : vendredi 12 avril 2013 - 11:20:23

Fichier

sikmhs.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00772757, version 1

Collections

INRIA

Citation

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〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

175

Téléchargements de fichiers

105

Contact


archive-ouverte@inria.fr