Publication details

Saarland University Computer Science

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               

Login to edit

Legal notice, Privacy policy