| |
VOLUME 2, ISSUE 5, PAPER 1
|
Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages
|
©Lars Birkedal, IT University of Copenhagen
©Noah Torp-Smith, IT University of Copenhagen
©Hongseok Yang, Seoul National University
|
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.
|
Publication date: November 3, 2006
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-2(5:1)2006
Hit Counts: 5334 |
 Creative Commons | |
