[PL-sem-jr] Monday, 10/20: separation logic

[Aaron Turon]

Here's the roster of upcoming talks:

10/20 *Tomorrow* Aaron on separation logic
10/27  Stephen, topic TBD
11/3  Dan, Call/cc + Curry-Howard

Talks are from 1-3pm in WVH 166.  We have an open slot for 11/17;
please email me if you are interested in filling it.

--

10/20 Separation logic
Abstract

Hoare logic was introduced in 1969 as a way to reduce reasoning about
programs to reasoning in first-order logic.  It's proof theory is,
crucially, compositional: proving that a compound program obeys its
specification depends only on proving that its subprograms obey their
specifications.  The original Hoare logic dealt with an imperative
while-language without pointers, but since then the essential ideas of
Hoare logic have been applied to construct new Hoare logics for a vast
variety of languages and language features.

In 1999-2001, Peter O'Hearn and John Reynolds simultaneously (but
separately) invented separation logic, a modification of Hoare logic
geared toward programs with pointers.  Separation logic modifies the
underlying first-order logic to include the "separating conjunction"
of two formulas, which holds when the heap can be split into two
disjoint sections, with one formula holding in the first section, and
the other, the second.  With this relatively simple addition, and some
new proof rules, the resulting logic provides a surprisingly elegant
and powerful way of reasoning about pointer programs (while ruling out
aliasing, etc).

I will spend the first part of the talk reviewing concepts from Hoare
logic and giving a few examples, before showing how things start to
break down when a heap is introduced.  Then I will present separation
logic in detail and work through several examples with various
pointer-based data structures.  Finally, if time permits, I will
briefly introduce concurrent separation logic, a recent development
that applies separation logic to reasoning about shared-state
concurrency.