Lars Birkedal ; Noah Torp-Smith ; Hongseok Yang - 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 - https://doi.org/10.2168/LMCS-2(5:1)2006
Semantics of Separation-Logic Typing and Higher-order Frame Rules for<br> Algol-like LanguagesArticle

Authors: Lars Birkedal ; Noah Torp-Smith ; Hongseok Yang

    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.


    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

    32 Documents citing this article

    Consultation statistics

    This page has been seen 2014 times.
    This article's PDF has been downloaded 329 times.