| Title: |
A step-indexed Kripke Model of Hidden State |
| Authors: |
Schwinghammer, Jan; Birkedal, Lars; Pottier, François; Reus, Bernhard; Støvring, Kristian; Yang, Hongseok |
| Contributors: |
Programming Systems Lab Saarland; Saarland University Saarbrücken; IT University of Copenhagen (ITU); Programming languages, types, compilation and proofs (GALLIUM); Inria Paris-Rocquencourt; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria); Department of Informatics Brighton; University of Sussex; Department of Computer Science Copenhagen (DIKU); Faculty of Science Copenhagen; University of Copenhagen = Københavns Universitet (UCPH)-University of Copenhagen = Københavns Universitet (UCPH); Computing Laboratory (OUCL); University of Oxford |
| Source: |
ISSN: 0960-1295. |
| Publisher Information: |
HAL CCSD; Cambridge University Press (CUP) |
| Publication Year: |
2013 |
| Collection: |
Archive ouverte HAL (Hyper Article en Ligne, CCSD - Centre pour la Communication Scientifique Directe) |
| Subject Terms: |
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] |
| Description: |
International audience ; 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: |
article in journal/newspaper |
| Language: |
English |
| Relation: |
hal-00772757; https://inria.hal.science/hal-00772757; https://inria.hal.science/hal-00772757/document; https://inria.hal.science/hal-00772757/file/sikmhs.pdf |
| Availability: |
https://inria.hal.science/hal-00772757; https://inria.hal.science/hal-00772757/document; https://inria.hal.science/hal-00772757/file/sikmhs.pdf |
| Rights: |
info:eu-repo/semantics/OpenAccess |
| Accession Number: |
edsbas.2F37AFEA |
| Database: |
BASE |