TY - RPRT
T1 - BI Hyperdoctrines, Higher-Order Separation Logic, and Abstraction
AU - Biering, Bodil
AU - Birkedal, Lars
AU - Torp-Smith, Noah
PY - 2005/7
Y1 - 2005/7
N2 - 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.
AB - 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.
M3 - Report
T3 - IT University Technical Report Series
BT - BI Hyperdoctrines, Higher-Order Separation Logic, and Abstraction
PB - IT-Universitetet i København
CY - Copenhagen
ER -