Towards a Semantic Characterisation of Global Type Well-formedness
Ilaria Castellani, Paola Giannini
TL;DR
The paper investigates how well-formedness properties of multiparty session types can be characterized semantically within Prime Event Structures. Building on prior ES-based semantics, it defines semantic notions of projectability and boundedness for PESs and proves three key results: that all global types typing the same network yield the same PES, that the semantic properties faithfully reflect the original well-formedness criteria, and that PESs arising from global types possess informative structural characteristics. These contributions enable reasoning about MPST well-formedness directly at the semantic level and pave the way for sanitising ill-formed global types via PES-based analysis. The work also discusses related denotational models and outlines future directions for a full characterization and potential synthesis from g-PESs.
Abstract
We address the question of characterising the well-formedness properties of multiparty session types semantically, i.e., as properties of the semantic model used to interpret types. Choosing Prime Event Structures (PESs) as our semantic model, we present semantic counterparts for the two properties that underpin global type well-formedness, namely projectability and boundedness, in this model. As a first step towards a characterisation of the class of PESs corresponding to well-formed global types, we identify some simple structural properties satisfied by such PESs.