Multiparty Classical Choreographies
Marco Carbone, Luis Cruz-Filipe, Fabrizio Montesi, Agata Murawska

TL;DR
Multiparty Classical Choreographies (MCC) is a language that unifies various approaches to communicating systems using linear logic, supporting server invocation and logic-driven compilation of replicated processes.
Contribution
MCC introduces a unified framework for multiparty choreographies based on linear logic, supporting server invocation and process replication.
Findings
Unifies different approaches to choreographies and processes
Supports server invocation in choreographies
Enables logic-driven compilation of replicated processes
Abstract
We present Multiparty Classical Choreographies (MCC), a language model where global descriptions of communicating systems (choreographies) implement typed multiparty sessions. Typing is achieved by generalising classical linear logic to judgements that explicitly record parallelism by means of hypersequents. Our approach unifies different lines of work on choreographies and processes with multiparty sessions, as well as their connection to linear logic. Thus, results developed in one context are carried over to the others. Key novelties of MCC include support for server invocation in choreographies, as well as logic-driven compilation of choreographies with replicated processes.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsMulti-Agent Systems and Negotiation · Logic, programming, and type systems · Logic, Reasoning, and Knowledge
