A Synthetic Reconstruction of Multiparty Session Types
summary
New approach types processes directly against a global labelled transition system, claiming no projection and restoring compositionality while matching the expressiveness of the “less‑is‑more” benchmark (previously non‑compositional examples become typable). Core results are mechanised and checked, with the theory formalised as mechanised in Agda and instantiated for well‑behaved LTS. Deliverables include a proof archive and a VS Code extension prototype; artifacts are available and evaluate as functional.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 1:25Problem in concurrent programming
- 3:54Session types fundamentals
- 8:08Projection limitations
- 9:12'Less is more' critique
- 10:17Direct global type checking
- 13:24Four steps to new type system
- 14:27Operational semantics of terms
- 15:29Operational semantics of types
- 16:12Typing rules for output
- 17:14Additional language features
- 18:38Novelty in synthetic typing
- 20:48Generalization to label transition systems
- 21:51Summary and future work
related talks
18mHybrid Multiparty Session Types: Compositionality for Protocol Specification th...
35mEvent-Driven Multiparty Session Actors
37mSession Types: A History and Applications
32mMulticompatibility for Multiparty-Session Composition
15mStatically Verified Refinements for Multiparty Protocols
37mUsing Event Structures to model Multiparty Session Types: results and open problems
15mA Multiparty Session Typing Discipline for Fault-tolerant Event-driven Distributed Programming
20mMessage-Observing Sessions