Separation logic is an extension of Hoare's logic oriented to reasoning about mutable data structures (or, programs with dynamically allocated pointers). It enables more compact proofs and specs of imperative programs than before because of its support for local reasoning, where specifications and proofs concentrate on the portion of memory used by a program component, and not the entire global state of the system.

The purpose of these pages is to give some context for people wanting to learn about the work. There is no attempt to be comprehensive or uptodate in these pages. And the material is undoubtedly biased, perhaps even a bit East London-centric. But you can find lots more information on the pages linked at the top, and further (especially current) information on the pages of people mentioned throughout, as well the links at the bottom.

News: As of late 2010 I am updating these pages only infrequently; there is too much interesting work happening for me to do justice to here, much of it of which is geographically distributed (where this page has a London-Cambridge leaning). For the absolute most recent happenings, places to look include the Resource Reasoning page, pages of folks from the East London Massive, or you can just consult a search engine.

Quick Start: A good way to get started is to read the CSL'01 paper which introduced the principle of local reasoning, and Reynolds's invited paper from LICS'02, together or in quick succession. When understanding a subject it is also helpful (and not emphasized enough in CS) to have a picture of the development of ideas. If you are interested in this sort of thing, go here for the early days.

Other Links:  Resource Reasoning project,  East London Massive