BI Hyperdoctrines, Higher-Order Separation Logic, and Abstraction

Bodil Biering
Lars Birkedal
Noah Torp-Smith

July 2005

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 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.

Technical report TR-2005-69 in IT University Technical Report Series, July 2005.

Available as PDF.