Abstract
Separation logic is a Hoare-style logic for reasoning about pointer-manipulating programs. Its core ideas have recently been extended from low-level to richer, high-level languages. In this paper we develop a new semantics of the logic for a programming language where code can be stored (i.e., with higher-order store). The main improvement on previous work is the simplicity of the model. As a consequence, several restrictions imposed by the semantics are removed, leading to a considerably more natural assertion language with a powerful specification logic.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Biering, B., Birkedal, L., Torp-Smith, N.: BI-hyperdoctrines, higher-order separation logic, and abstraction. ACM TOPLAS 29(5) (2007)
Birkedal, L., Torp-Smith, N., Yang, H.: Semantics of separation-logic typing and higher-order frame rules for algol-like languages. LMCS 2(5-1) (2006)
Birkedal, L., Yang, H.: Relational parametricity and separation logic. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423. Springer, Heidelberg (2007)
Cai, H., Shao, Z., Vaynberg, A.: Certified self-modifying code. In: Proc. PLDI 2007, pp. 66–77 (2007)
Corbet, J., Rubini, A., Kroah-Hartman, G.: Linux Device Drivers, 3rd edn. O’Reilly, Sebastopol (2005)
Honda, K., Yoshida, N., Berger, M.: An observationally complete program logic for imperative higher-order functions. In: Proc. LICS 2005, pp. 270–279 (2005)
Krishnaswami, N., Aldrich, J., Birkedal, L.: Modular verification of the subject-observer pattern via higher-order separation logic. In: FTfJP 2007 (2007)
Nanevski, A., Ahmed, A., Morrisett, G., Birkedal, L.: Abstract predicates and mutable ADTs in Hoare type theory. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 189–204. Springer, Heidelberg (2007)
Nanevski, A., Morrisett, G., Birkedal, L.: Polymorphism and separation in Hoare type theory. In: Proc. ICFP 2006, pp. 62–73 (2006)
O’Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1–18. Springer, Heidelberg (2001)
O’Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: Proc. of 31st POPL, pp. 268–280 (2004)
Parkinson, M.: When separation logic met Java. In: FTfJP 2006 (2006)
Parkinson, M., Bierman, G.: Separation logic, abstraction and inheritance. In: Proc. 35th POPL (2008)
Pitts, A.M.: Relational properties of domains. Information and Computation 127, 66–90 (1996)
Reus, B., Schwinghammer, J.: Separation logic for higher-order store. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 575–590. Springer, Heidelberg (2006)
Reus, B., Streicher, T.: About Hoare logics for higher-order store. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1337–1348. Springer, Heidelberg (2005)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. LICS 2002, pp. 55–74 (2002)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Birkedal, L., Reus, B., Schwinghammer, J., Yang, H. (2008). A Simple Model of Separation Logic for Higher-Order Store. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds) Automata, Languages and Programming. ICALP 2008. Lecture Notes in Computer Science, vol 5126. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70583-3_29
Download citation
DOI: https://doi.org/10.1007/978-3-540-70583-3_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70582-6
Online ISBN: 978-3-540-70583-3
eBook Packages: Computer ScienceComputer Science (R0)