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.
Barwell, Ping Hou, Nobuko Y oshida & Fangyi Zhou (2 025): Crash-Stop Failures in Asynchronous Multiparty Session Types
2 Pith papers cite this work. Polarity classification is still indexing.
2
Pith papers citing it
years
2026 2representative citing papers
The work defines enriched global types for multiparty session types that incorporate failure semantics and dynamic participation, proves coherence preservation, and positions the framework as a foundation for stateful and liveness verification in web applications.
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.
-
Towards Multiparty Session Types for Highly-Concurrent and Fault-Tolerant Web Applications
The work defines enriched global types for multiparty session types that incorporate failure semantics and dynamic participation, proves coherence preservation, and positions the framework as a foundation for stateful and liveness verification in web applications.