BI Hyperdoctrines, Higher-Order Separation Logic, and Abstraction

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 fact that this is a useful extension is illustrated via examples; specifically we demonstrate that existential and universal quantification correspond to abstract data types and parametric data types, respectively. We also illustrate that the semantics we give is an instance of a general notion, namely that of a BI hyperdoctrine, of models for predicate BI.