Multiparty symmetric sum types

Abstract

This paper extends the multiparty asynchronous session types to symmetric sumtypes, which can type non-deterministic orchestration choice behaviours. While the original branching in the session types requires one participant to decide how to proceed by sending a label, with symmetric sumtypes the choice can be made in a non-deterministic way by synchronisation between the participants in a multiparty session. The motivation for synchronisation comes from natural and concise modelling of social interaction and cooperation in healthcare scenarios in the Process Matrix. The behaviour of synchronisation is represented by a new synchronise process constructor, which is typed by symmetric sumtypes. Finally we show that symmetric sumtypes can be erased into the original branching types with the help of conductor processes, preserving typability and operational semantics.