Sciweavers

Share
LICS
2008
IEEE

Hiding Local State in Direct Style: A Higher-Order Anti-Frame Rule

9 years 9 months ago
Hiding Local State in Direct Style: A Higher-Order Anti-Frame Rule
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 direct style. 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.
François Pottier
Added 31 May 2010
Updated 31 May 2010
Type Conference
Year 2008
Where LICS
Authors François Pottier
Comments (0)
books