Higher-Order Separation Logic and Abstraction

Abstract. We present a simple extension of separation logic which makes the specification language higher order, in the sense that quantification over predicates and higher types is possible. The force of this extension is illustrated via examples; specifically we demonstrate that existential and universal quantification correspond to abstract data types and parametric data types, respectively. Moreover, we show how to express invariance of programs in our framework