Birkedal, Lars and Torp-Smith, Noah and Yang, Hongseok - Semantics of Separation-Logic Typing and Higher-order Frame Rules for<br> Algol-like Languages

lmcs:2232 - Logical Methods in Computer Science, November 3, 2006, Volume 2, Issue 5
Semantics of Separation-Logic Typing and Higher-order Frame Rules for<br> Algol-like Languages

Authors: Birkedal, Lars and Torp-Smith, Noah and Yang, Hongseok

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.


Source : oai:arXiv.org:cs/0610081
DOI : 10.2168/LMCS-2(5:1)2006
Volume: Volume 2, Issue 5
Published on: November 3, 2006
Submitted on: December 21, 2005
Keywords: Computer Science - Logic in Computer Science,F.3,D.3


Share

Consultation statistics

This page has been seen 314 times.
This article's PDF has been downloaded 17 times.