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
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.
95 ms
(Ver 3.3 (11022016))