Analyzing Multiparty Interaction using Conversation Types

Hugo Torres Vieira, Universidade Nova de Lisboa, Portugal

We present conversation types, an extension of binary session types that support the analysis of concurrent multiparty interaction. While initially developed for the conversation calculus, we show that our type discipline is general enough to be adapted to other models. In particular, this talk addresses systems specified in the pi-calculus extended with labeled communication, exploiting the distinction between such labels to discipline interaction between multiple parties in a single communication medium. We also present a complementary technique to ensure progress of systems, based on well-founded ordering of events. Our approach addresses challenging scenarios where participants dynamically join and leave conversations and interleave their participation in several conversations, including dynamically established ones. We prove well-typed and well-ordered systems never violate the prescribed conversation constraints and never deadlock.