BI hyperdoctrines and higher-order separation logic

Abstract

We present a precise correspondence between separation logic and a new simple notion of predicate BI, extending the earlier correspondence given between part of separation logic and propositional BI [14]. Moreover, we introduce the notion of a BI hyperdoctrine and show that it soundly models classical and intuitionistic first- and higher-order predicate BI, and use it to show that we may easily extend separation logic to higher-order. We argue that the given correspondence may be of import for formalizations of separation logic. © Springer-Verlag Berlin Heidelberg 2005.