loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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
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.