@book{89fb597351d740cda31e32b63410e384,
title = "BI Hyperdoctrines, 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 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. ",
keywords = "Separation logic, Higher-order logic, BI hyperdoctrine, Predicate BI, Abstract data types",
author = "Bodil Biering and Lars Birkedal and Noah Torp-Smith",
year = "2005",
month = jul,
language = "English",
series = "IT University Technical Report Series",
number = "TR-2005-69",
publisher = "IT-Universitetet i K{\o}benhavn",
address = "Denmark",
edition = "TR-2005-69",
}