Abstract
Separation logic is a recent extension of Hoare logic for reasoning about programs with references to shared mutable data structures. In this paper, we provide a new interpretation of the logic for a programming language with higher types. Our interpretation is based on Reynolds’s relational parametricity, and it provides a formal connection between separation logic and data abstraction.
This work was supported by FUR (FIRST). Yang was supported also by EPSRC. We would like to thank Nick Benton for his insightful comments.
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
Barnett, M., Naumann, D.: Towards imperative modules: Reasoning about invariants and sharing of mutable state. In: Proc. of LICS’04 (2004)
Benton, N.: Abstracting Allocation: The New new Thing. In: Proc. of CSL’06 (2006)
Benton, N., Leperchey, B.: Relational reasoning in a nominal semantics for storage. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 88–101. Springer, Heidelberg (2005)
Biering, B., Birkedal, L., Torp-Smith, N.: BI-hyperdoctrines and higher order separation logic. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 233–247. Springer, Heidelberg (2005)
Birkedal, L., Møgelberg, R.: Categorical models for Abadi-Plotkin’s logic for parametricity. Mathematical Structures in Computer Science 15, 709–772 (2005)
Birkedal, L., Torp-Smith, N., Reynolds, J.C.: Local reasoning about a copying garbage collector. In: Proc. of POPL’04, Venice, Italy, pp. 220–231 (2004)
Birkedal, L., Torp-Smith, N., Yang, H.: Semantics of separation-logic typing and higher-order frame rules. In: Proc. of LICS’05, pp. 260–269 (2005)
Mijajlović, I., Torp-Smith, N., O’Hearn, P.: Refinement and separation context. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 421–433. Springer, Heidelberg (2004)
Mijajlović, I., Yang, H.: Data refinements with low-level pointer operations. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 19–36. Springer, Heidelberg (2005)
O’Hearn, P., Reynolds, J.: From Algol to polymorphic linear lambda-calculus. Journal of the ACM 47(1), 167–223 (2000)
Yang, H., O’Hearn, P.W., Reynolds, J.C.: Local Reasoning about Programs that Alter Data Structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, Springer, Heidelberg (2001)
O’Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: Proc. of POPL’04, Venice, Italy, pp. 268–280 (2004)
Parkinson, M., Bierman, G.: Separation logic and abstraction. In: Proc. of POPL’05, Long Beach, CA, USA, pp. 247–258 (2005)
Plotkin, G., Abadi, M.: A logic for parametric polymorphism. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 361–375. Springer, Heidelberg (1993)
Reynolds, J.: Types, abstraction, and parametric polymorphism. Information Processing 83, 513–523 (1983)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. of LICS’02, Copenhagen, Denmark, pp. 55–74 (2002)
Shinwell, M.R., Pitts, A.M.: On a monadic semantics for freshness. Theoretical Computer Science 342, 28–55 (2005)
Torp-Smith, N.: Advances in Separation Logic — A Study of Logics for Reasoning about Stateful Programs. PhD thesis, IT University of Copenhagen (2005)
Yang, H.: Relational separation logic. Theoretical Comput. Sci. (to appear, 2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Birkedal, L., Yang, H. (2007). Relational Parametricity and Separation Logic. In: Seidl, H. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2007. Lecture Notes in Computer Science, vol 4423. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71389-0_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-71389-0_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71388-3
Online ISBN: 978-3-540-71389-0
eBook Packages: Computer ScienceComputer Science (R0)