Abstract
Multiparty session types (MSTs) are a type-based approach to reasoning about communication protocols.
Central to MSTs is a projection operator: a partial function that synthesizes a correct-by-construction distributed implementation from a high-level protocol represented as a global type.
Most projection operators in existing work are syntactic in nature, and trade efficiency for completeness. In the talk, I will present the first projection operator that is sound and complete. I will highlight the automata-theoretic nature of our projection operator, and show how implementability can be checked directly on the candidate implementations it computes.