Certifying Data in Multiparty Session Types

Bernardo Toninho

Imperial College London


Multiparty session types are a typing discipline and methodology to
ensure communication safety in protocols involving two or more
concurrent participants.

In this talk I will present the integration of value dependent types
in a multiparty session typed framework (i.e. types that depend on the
exchanged data values), enabling static assurances of not only
communication safety but also of properties of the data itself.
I will discuss the main tensions, challenges and trade-offs of
adopting such a framework in the context of multiparty conversations,
as well as a few simple extensions that increase the flexibility and
expressiveness of the framework such as so-called “ghost variables” and
provenance information tracking in a distributed setting.

I will also elaborate on some potential avenues of future research based
on this framework.

Thursday, December 17 2015