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

TL;DR

This paper develops a coherent semantic framework for higher-order separation logic in an Algol-like language, enabling sound reasoning with higher-order frame rules for local reasoning about programs with heaps.

Contribution

It introduces a semantic model for higher-order separation logic in an idealized Algol language, including sound rules for higher-order frame rules.

Findings

Semantic model for higher-order separation logic

Sound higher-order frame rules established

Supports local reasoning in heap-manipulating programs

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.