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 with heaps (but immutable stack
variables). In particular, we provide simple and sound rules for
deriving higher-order frame rules, allowing for local reasoning.
|