Lars Birkedal: "An Introduction to Separation Logic, and the
Benefits of going Higher-order
(A Tutorial)" in the Seminar Series 2013 of the IRIT "Logics and analyses for verifying graph transformation" and as preparation for the Types 2013 meeting, April 22, 2013 in Toulouse)
Separation logic is a program logic for reasoning about programs
with shared mutable state. Crucially, it supports modular reasoning
because specifications and proofs can concentrate on the memory
resources that a program actually acts upon, instead of its entire
global state. Separation logic can logically distinguish between
situations where memory is shared and where it is not. That makes
reasoning much simpler in all those cases where there is separation
(no sharing) and hence no important interactions. Separation logic
was originally developed for reasoning about low-level languages
with mutable shared data structures. As a step towards reasoning
about more high-level programs, we developed a higher-order version
of separation logic and showed how it could be used for modular
reasoning about abstract data types and higher-order functions.
In this tutorial I will give a gentle introduction to separation logic,
explaining the key ideas and also sketch how higher-order separation
logic is useful for reasoning about abstract data types.
To make it easier to understand other recent developments related
to separation logic for languages with concurrency, I will explain how
the standard model of separation logic can be seen as an instance
of the recently proposed Concurrent Views Framework presented at POPL 2013.