IMDEA Software

IMDEA initiative

Home > Events > Invited Talks > 2010 > On Separation, Session Types and Algebra

Peter O'Hearn

Thursday, December 2, 2010

10:00am IMDEA conference room

Peter O'Hearn, Professor, Queen Mary, London University

On Separation, Session Types and Algebra

Abstract:

This talk explores the relation between two formalisms and one algebraic framework for concurrency. Session Types and Concurrent Separation Logic are formalisms that support independent reasoning about concurrent processes. We first translate a small language we call Baby Session Types (BST), into a “basic” version of Concurrent Separation Logic (BCSL), and we show that the translation is sound and complete. We then describe a model for BCSL (hence, BST), which exhibits an algebraic structure of two semigroups (for sequential and parallel composition) linked by an exchange law as advanced recently in Concurrent Kleene Algebra. The model construction is very general, starting from any partial commutative monoid of propositions. However, an instantiation where Session Type contexts are the propositions provides a natural model of and concrete meaning to a notion of Hoare triples in the algebra models, corresponding to the intuition of a typing (assertion) as providing an over-approximation of the future.