Paper: Hiding Local State in Direct Style: A Higher-Order Anti-Frame Rule (at LICS 2008)

Authors: François Pottier

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.

BibTeX

  @InProceedings{Pottier-HidingLocalStateinD,
    author = 	 {François Pottier},
    title = 	 {Hiding Local State in Direct Style: A Higher-Order Anti-Frame Rule},
    booktitle =  {Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science (LICS 2008)},
    year =	 {2008},
    month =	 {June}, 
    pages =      {331--340},
    location =   {Pittsburgh, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }