Semantics of Separation-Logic Typing and Higher-order Frame Rules for<br> Algol-like Languages
Logic in Computer Science
2017-01-11 v2
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.
Cite
@article{arxiv.cs/0610081,
title = {Semantics of Separation-Logic Typing and Higher-order Frame Rules for<br> Algol-like Languages},
author = {Lars Birkedal and Noah Torp-Smith and Hongseok Yang},
journal= {arXiv preprint arXiv:cs/0610081},
year = {2017}
}