Peter O'Hearn
Queen Mary, University of London
On the
Relation between Session Types and Concurrent Separation Logic
Abstract:
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 <tracyf@cs.cmu.edu>
Tuesday, May 26, 2009
3:30 p.m.
Wean
Hall 4623
Principles
of Programming Seminars