Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages

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.

• Type: Journal
• Year: 2006
• Where: LMCS
• Authors: Lars Birkedal, Noah Torp-Smith, Hongseok Yang
• Keywords: Coherent Semantics, Immutable Stack, LMCS 2006, Simple Sound Rules