Using Event Structures to model Multiparty Session Types: results and open problems
summary
Event Structures are used as a denotational semantics for multiparty session types, producing isomorphic domains of configurations whenever a network is typable by a global type; the synchronous case is published and the asynchronous variant is under submission. The work builds a concrete mapping using flow event structures (a generalization of prime ES) so that networks and global types yield the same configuration domains, gives semantic counterparts for syntactic well‑formedness and boundedness, and shows deadlock states collapse to empty configurations.
AI-written summary · about
chapters (13)
- 0:00Event structures and MPST intro
- 5:45Quick tour on event structures
- 10:08Prime event structures limits
- 12:22Flow event structures solution
- 16:16Configurations and domains
- 17:43Multiparty session calculus
- 19:07Well-formedness in global types
- 23:01Event structure semantics networks
- 25:54Event structure semantics global types
- 28:23Results and benefits
- 31:39Well-formedness semantics
- 32:44Related work and conclusions
- 33:05Q&A
related talks
37mSession Types: A History and Applications
23mA Synthetic Reconstruction of Multiparty Session Types
35mEvent-Driven Multiparty Session Actors
18mHybrid Multiparty Session Types: Compositionality for Protocol Specification th...
20mMessage-Observing Sessions
15mA Multiparty Session Typing Discipline for Fault-tolerant Event-driven Distributed Programming
32mMulticompatibility for Multiparty-Session Composition
38mEvent Design & Event-first Development