CoMPSeT: A Framework for Comparing Multiparty Session Types
Telmo Ribeiro, José Proença, Mário Florido
TL;DR
CoMPSeT addresses the challenge of a fragmented MPST landscape by delivering a browser-based, open-source tool built on the CAOS framework to configure, visualize, and compare MPST formalisms across different features such as merge criteria, communication models, and recursion schemes. The approach parametrises MPST components (global/local types, projections, and SOS semantics) and enables side-by-side semantic comparisons with runtime widget configurability and bisimulation checks. Core contributions include the CoMPSeT prototype, CAOS extensions for dynamic widgets and a Settings DSL/API, and illustrative use-cases demonstrating how semantic choices affect behavior and verification. The work advances accessibility and clarity in MPST research and pedagogy by providing interactive, visual exploration of how formal choices shape system safety, liveness, and communication patterns.
Abstract
Concurrent systems are often complex and difficult to design. Choreographic languages, such as Multiparty Session Types (MPST), allow the description of global protocols of interactions by capturing valid patterns of interactions between participants. Many variations of MPST exist, each one with its rather specific features and idiosyncrasies. Here we propose a tool (CoMPSeT) that provides clearer insights over different features in existing MPST. We select a representative set of MPST examples and provide mechanisms to combine different features and to animate and compare the semantics of concrete examples. CoMPSeT is open-source, compiled into JavaScript, and can be directly executed from any browser, becoming useful both for researchers who want to better understand the landscape of MPST and for teachers who want to explain global choreographies.