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

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>

Appointments: Tracy Farbacher <tracyf@cs.cmu.edu>

Tuesday, May 26, 2009

3:30 p.m.

Wean Hall 4623

Principles
of Programming Seminars