loading...
Semantics of Separation-Logic Typing and Higher-Order Frame Rules
Chicago, Illinois June 26-June 29
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2005.4720th Annual IEEE Symposium on Logic i ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Lars Birkedal, IT University of Copenhagen
Noah Torp-Smith, IT University of Copenhagen
Hongseok Yang, Seoul National University
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.
Citation:
Lars Birkedal, Noah Torp-Smith, Hongseok Yang, "Semantics of Separation-Logic Typing and Higher-Order Frame Rules," lics, pp.260-269, 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05), 2005
Usage of this product signifies your acceptance of the Terms of Use.