Peter O'Hearn
Queen Mary, University of London

On the Relation between Session Types and Concurrent Separation Logic

Concurrent separation logic provides a modular way of reasoning about shared-memory programs, where sequential reasoning is valid when not
at synchronization points. Typing systems based on pi-calculus have been developed which allow for modular proofs of certain message-passing idioms. These systems of `session types'   use typing rules inspired by linear logic to divide the channel ends amongst processes, where concurrent separation logic divides heap cells amongst processes. In this talk I describe an attempt to link these two lines of work.

This talk describes joint work with Akbar Hussain and Rasmus Petersen

Host: John Reynolds
Appointments: Tracy Farbacher <>

Tuesday, May 26, 2009

3:30 p.m.
Wean Hall 4623

Principles of Programming Seminars