An Introduction to Separation Logic, and the Benefits of going Higher-order (A Tutorial)

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.