Paper: Semantics of Separation-Logic Typing and Higher-Order Frame Rules (at LICS 2005)

Authors: Lars Birkedal Noah Torp-Smith Hongseok Yang

Abstract

We show how to give a coherent semantics to programs that are well-specified in a version of separation logic for a language with higher types: idealized algol extended with heaps (but with immutable stack variables). In particular, we provide simple sound rules for deriving higher-order frame rules, allowing for local reasoning.

BibTeX

  @InProceedings{BirkedalTorpSmithYa-SemanticsofSeparati,
    author = 	 {Lars Birkedal and Noah Torp-Smith and Hongseok Yang},
    title = 	 {Semantics of Separation-Logic Typing and Higher-Order Frame Rules},
    booktitle =  {Proceedings of the Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS 2005)},
    year =	 {2005},
    month =	 {June}, 
    pages =      {260--269},
    location =   {Chicago, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }