EVENT

Talk by Prof. Nobuko Yoshida from Imperial College London :"Synthesis of Multiparty Session Types"

Outline

Speaker

Nobuko Yoshida (Imperial College London)
http://mrg.doc.ic.ac.uk/

Date:

July 19 (Tue.), 2016

Time:

10:00-12:00

Place:

National Institute of Informatics (NII)
20th floor, Room 2005 (Lecture Room 1)

Title:

Synthesis of Multiparty Session Types

Abstract:

Multiparty session types are a type system that can ensure the safetyand liveness of distributed peers via the global specification oftheir interactions. To construct a global specification from a set ofdistributed uncontrolled behaviours, this talk explores the problem offully characterising multiparty session types in terms ofcommunicating automata. We equip global and local session types withlabelled transition systems (LTSs) that faithfully representasynchronous communications through unbounded buffered channels. Usingthe equivalence between the two LTSs, we identify a class ofcommunicating automata that exactly correspond to the projected localtypes. We exhibit an algorithm to synthesise a global type from acollection of communicating automata. The key property of our findingsis the notion of multiparty compatibility which non-trivially extendsthe duality condition for binary session types.At the end of the talk, I also show a couple of applications of the synthesis theory of multiparty session types.