Cambridge Concurrency Workshop
5th - 6th July 2010

Concurrency at the Abstract Level

Separation Logic (O'Hearn et al.) provides local reasoning about programs that manipulate a low-level heap. Not only has it been used with great success to reason about sequential programs, but it has also been extended, in a variety of ways, to reason about programs with concurrent behaviour, whilst still adhering to the ideals of local reasoning. 
Context Logic (Gardner et al.) was introduced to generalise the ideas of Separation Logic to higher levels of data abstraction. This has most notably been used to provide a local, formal and compositional version of the W3C DOM specification. However, the concept of splitting program data into a context and some sub-data  does not extend well to the concurrent setting.
We have recently introduced Segment Logic to provide a more fine-grained notion of splitting up program data at the high level. We shall introduce Segment Logic and show how the low-level concurrency rules from Separation Logic can be interpreted at the high-level.