Logic in Computer Science, Symposium on (2008)
June 24, 2008 to June 27, 2008
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2008.16
Separation logic involves two dual forms of modularity: local reasoning makes part of the store invisible within a static scope, whereas hiding local state makes part of the store invisible outside a static scope.??In the recent literature, both idioms are explained in terms of a higher-order frame rule. I point out that this approach to hiding local state imposes continuation-passing style, which is impractical. Instead, I introduce a higher-order anti-frame rule, which permits hiding local state in directstyle. I formalize this rule in the setting of a type system, equipped with linear capabilities, for an ML-like programming language, and prove type soundness via a syntactic argument.??Several applications illustrate the expressive power of the new rule.
Proofs of programs, dynamic memory allocation, separation logic, hidden local state, higher-order frame rule
F. Pottier, "Hiding Local State in Direct Style: A Higher-Order Anti-Frame Rule," 23rd Annual IEEE Symposium on Logic in Computer Science (LICS 2008)(LICS), Pittsburgh, PA, 2008, pp. 331-340.