The Community for Technology Leaders
Logic in Computer Science, Symposium on (2008)
June 24, 2008 to June 27, 2008
ISSN: 1043-6871
ISBN: 978-0-7695-3183-0
pp: 331-340
ABSTRACT
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", Logic in Computer Science, Symposium on, vol. 00, no. , pp. 331-340, 2008, doi:10.1109/LICS.2008.16
98 ms
(Ver 3.3 (11022016))