2008 23rd Annual IEEE Symposium on Logic in Computer Science Hiding Local State in Direct Style: A Higher-Order Anti-Frame Rule June 24-June 27 ISBN: 978-0-7695-3183-0
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.
Index Terms:
Proofs of programs, dynamic memory allocation, separation logic, hidden local state, higher-order frame rule
Citation:
Francois Pottier, "Hiding Local State in Direct Style: A Higher-Order Anti-Frame Rule," lics, pp.331-340, 2008 23rd Annual IEEE Symposium on Logic in Computer Science, 2008 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||