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. © 2008 Springer-Verlag.
Cite
CITATION STYLE
Birkedal, L., Reus, B., Schwinghammer, J., & Yang, H. (2008). A simple model of separation logic for higher-order store. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5126 LNCS, pp. 348–360). https://doi.org/10.1007/978-3-540-70583-3_29
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
