Semantics of Separation-Logic Typing and Higher-order Frame Rules for<br> Algol-like Languages
classification
💻 cs.LO
keywords
rulesframehigher-ordersemanticsalgolalgol-likeallowingcoherent
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.