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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Biering, B.: On the logic of bunched implications and its relation to separation logic. Master’s thesis, University of Copenhagen (2004)
Birkedal, L., Torp-Smith, N., Reynolds, J.C.: Local reasoning about a copying garbage collector. In: Proceedings of the 31-st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2004), Venice, Italy, pp. 220–231 (2004)
Bornat, R.: Local reasoning, separation and aliasing. In: Proceedings of the Second Workshop on Semantics, Program Analysis and Computing Environments for Memory Management (SPACE 2004), Venice, Italy (January 2004)
Bornat, R., Calcagno, C., O’Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: Proceedings of POPL 2005, Long Beach, CA, USA, January 2005. ACM, New York (2005) Accepted for publication
Calcagno, C., O’Hearn, P.W., Bornat, R.: Program logic and equivalence in the presence of garbage collection. Theoretical Computer Science 298(3), 557–587 (2003)
Ishtiaq, S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2001 (2001)
Jacobs, B.: Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics, vol. 141. North-Holland Publishing Co., Amsterdam (1999)
Lawvere, F.W.: Adjointness in foundations. Dialectica 23(3/4), 281–296 (1969)
O’Hearn, P.W., Yang, H., Reynolds, J.C.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001)
O’Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding (work in progress). Extended version of [11] (2003)
O’Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: Proceedings of the 31-st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2004), Venice, Italy, pp. 268–280 (2004)
O’Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bulletin of Symbolic Logic 5(2), 215–244 (1999)
Pitts, A.M.: Categorical logic. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Algebraic and Logical Structures Handbook of Logic in Computer Science, ch. 2, vol. 5. Oxford University Press, Oxford (2000)
Pym, D., O’Hearn, P.W., Yang, H.: Possible worlds and resources: The semantics of BI. Theoretical Computer Science 315(1), 257–305 (2004)
Pym, D.J.: The Semantics and Proof Theory of the Logic of Bunched Implications. Kluwer Academic Publishers, Dordrecht (2002)
Pym, D.J.: Errata and remarks for the semantics and proof theory of the logic of bunched implications (2004), Available at http://www.cs.bath.ac.uk/~pym/BI-monograph-errata.pdf
Reynolds, J.C.: On extensions of separation logic. Private Communication
Reynolds, J.C.: The Craft of Programming. Prentice-Hall, Englewood Cliffs (1981)
Reynolds, J.C.: Intuitionistic reasoning about shared mutable data structure. In: Davies, J., Roscoe, B., Woodcock, J. (eds.) Millennial Perspectives in Computer Science, pp. 303–321. Palgrave, Houndsmill, Hampshire (2000)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Seventeenth Annual IEEE symposium on Logic in Computer Science (LICS 2002), Copenhagen, Denmark, pp. 55–74 (2002)
Yang, H.: Local Reasoning for Stateful Programs. PhD thesis, University of Illinois, Urbana-Champaign (2001)
Yang, H., Reddy, U.: Correctness of data representations involving heap data structures. Science of Computer Programming 50(1), 129–160 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Biering, B., Birkedal, L., Torp-Smith, N. (2005). BI Hyperdoctrines and Higher-Order Separation Logic. In: Sagiv, M. (eds) Programming Languages and Systems. ESOP 2005. Lecture Notes in Computer Science, vol 3444. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31987-0_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-31987-0_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25435-5
Online ISBN: 978-3-540-31987-0
eBook Packages: Computer ScienceComputer Science (R0)