The paper provides a 14K-line Rocq proof of safety and liveness for MPST via coinductive global/local types, operational correspondence, and mechanized projection/subtyping relations.
P ACMPL 3 (POPL), pp
3 Pith papers cite this work. Polarity classification is still indexing.
3
Pith papers citing it
fields
cs.LO 3representative citing papers
An asynchronous multiparty session calculus with mixed choice is equipped with a coherence-based type system using coinductive global types, proving subject reduction, session fidelity, lock-freedom, and orphan-message-freedom.
New global types for asynchronous multiparty sessions are interpreted as Prime Event Structures with equivalence to session interpretations as Flow Event Structures when typable.
citing papers explorer
-
Formally Verified Liveness with Multiparty Session Types in Rocq
The paper provides a 14K-line Rocq proof of safety and liveness for MPST via coinductive global/local types, operational correspondence, and mechanized projection/subtyping relations.
-
Asynchronous Multiparty Sessions with Mixed Choice
An asynchronous multiparty session calculus with mixed choice is equipped with a coherence-based type system using coinductive global types, proving subject reduction, session fidelity, lock-freedom, and orphan-message-freedom.
-
Global types and event structure semantics for asynchronous multiparty sessions
New global types for asynchronous multiparty sessions are interpreted as Prime Event Structures with equivalence to session interpretations as Flow Event Structures when typable.