Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

A Step-indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces

Lars Birkedal, Jan Schwinghammer, Kristian Støvring

Fixed Points in Computer Science (FICS'10), August 2010

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 give a possible worlds semantics for Chargueraud and Pottier's type and capability system including frame and anti-frame rules, based on the operational semantics and step-indexed heap relations. The worlds are constructed as a recursively defined predicate on a recursively defined metric space, which provides a considerably simpler alternative compared to a previous construction.

Download PDF        Show BibTeX               

@MISC{BirkedalEtAl:2010:A-Step-indexed,
  title = {A Step-indexed Kripke Model of Hidden State via  Recursive Properties on Recursively Defined Metric Spaces},
  author = {Lars Birkedal and Jan Schwinghammer and Kristian Støvring},
  year = {2010},
  month = {Aug},
  booktitle = {Fixed Points in Computer Science (FICS'10)},
  howpublished = {Informal workshop proceedings},
}

Login to edit