BI hyperdoctrines and higher-order separation logic

27Citations
Citations of this article
6Readers
Mendeley users who have this article in their library.

This article is free to access.

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.

Cite

CITATION STYLE

APA

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

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free