Copenhagen Programming Language Seminar


Separation Logic: A Logic for Shared Mutable Data Structures

John Reynolds
Computer Science Department, Carnegie Mellon University, USA

Thursday, December 19th, 15:15-16:00
IT-C, Glentevej 67, room 1.60


In joint work with Peter O'Hearn and others, based on early ideas of Burstall, we have developed an extension of Hoare logic that permits reasoning about low-level imperative programs that use shared mutable data structure.

The simple imperative programming language is extended with commands (not expressions) for accessing and modifying shared structures, and for explicit allocation and deallocation of storage. Assertions are extended by introducing a ``separating conjunction'' that asserts that its subformulas hold for disjoint parts of the heap, and a closely related ``separating implication''. Coupled with the inductive definition of predicates on abstract data structures, this extension permits the concise and flexible description of structures with controlled sharing.

In this talk, we will survey the current development of this program logic, including extensions that permit unrestricted address arithmetic, dynamically allocated arrays, and recursive procedures. We will also discuss promising future directions.

Scientific host: Lars Birkedal. Administrative host: Camilla Jørgensen. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, IT-C and KVL.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org