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.
CITATION STYLE
Biering, B., Birkedal, L., & Torp-Smith, N. (2005). BI hyperdoctrines and higher-order separation logic. In Lecture Notes in Computer Science (Vol. 3444, pp. 233–247). Springer Verlag. https://doi.org/10.1007/978-3-540-31987-0_17
Mendeley helps you to discover research relevant for your work.