A Step-Indexed Kripke Model of Hidden State Via Recursive Properties on Recursively Defined Metric Spaces

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. The authors 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.