Abstract

Separation Logic is a sub-structural logic that supports local reasoning for imperative programs with heaps. It is designed to elegantly describe sharing and aliasing properties of heap structures, thus facilitating the verification of programs with pointers. So far, various flavours of separation logic have been developed for heaps containing records of basic data types. Yet, languages like C or ML also allow procedures to be stored on the heap. Such type of heap is commonly referred to as “higher-order store’’. > This talk addresses the problem of lifting Separation Logic from first-order to higher-order store. To that end we endow a simple language including dynamic memory management with a Hoare-style logic featuring Separation Logic connectives. To prove soundness, Denotational Semantics is employed throughout but not just for conceptual clarity. Modeling higher-order store as recursive domain enables us to use powerful (and well established) results from Domain Theory. This approach also admits an elegant re-use of a proof rule we introduced in previous work to deal with recursion through the store.

This is joint work with Jan Schwinghammer, Programming Systems Lab, Saarland University.