The Logic of Separation Logic: Models and Proofs

Lecture notes in computer science, pp. 407–426

Abstract

Abstract The standard semantics of separation logic is restricted to finite heaps. This restriction already gives rise to a logic which does not satisfy compactness, hence it does not allow for an effective, sound and complete axiomatization. In this paper we therefore study both the general model theory and proof theory of the separation logic of finite and infinite heaps over arbitrary (first-order) models. We show that we can express in the resulting logic finiteness of the models and the existence of both countably infinite and uncountable models. We further show that a sound and complete sequent calculus still can be obtained by restricting the second-order quantification over heaps to first-order definable heaps.

Authors 3

1. Frank S. de Boer Aachen Leiden Institute of Advanced Computer Sciences (LIACS)

   Leiden University · Centrum Wiskunde & Informatica

   Affiliation as printed

   Centrum Wiskunde and Informatica (CWI), Amsterdam, The Netherlands

   Leiden Institute of Advanced Computer Sciences (LIACS), Leiden, The Netherlands

2. Hans-Dieter A. Hiep corresponding Aachen Leiden Institute of Advanced Computer Sciences (LIACS)

   Leiden University · Centrum Wiskunde & Informatica

   Affiliation as printed

   Centrum Wiskunde and Informatica (CWI), Amsterdam, The Netherlands

   Leiden Institute of Advanced Computer Sciences (LIACS), Leiden, The Netherlands

3. Stijn de Gouw

   Open University of the Netherlands

   Affiliation as printed

   Open University (OU), Heerlen, The Netherlands