Category:

Vlog

Duration: 1:06:45

59 views

0

Higher order frame rules in separation logic provide a way to understand disciplines such as ownership for information hiding in object based programs. Recent work of Banerjee, Naumann, and Rosenberg uses explicit regions to express, in classical first-order assertions, the read-footprints of predicates and write-footprints of commands, supporting an ordinary frame rule. On this basis, I give a second order frame rule, show its admissibility, and describe its use in encoding disciplines like ownership.