Mechanising Multiparty Session Types: A Sound and Complete Projection
summary
Defines a new computable projection for multiparty session types and proves it is both sound and complete with respect to the original coinductive counterpart, resolving cases where recursion plus branching made earlier projections fail. Provides an algorithm that computes a candidate local type then runs a decidable validation step (unfolding at most twice) and mechanises all proofs in Coq mechanisation (about 5,000 LOC), plus an unraveling theorem linking inductive and coinductive representations.
AI-written summary · about
chapters (10)
- 0:00Mechanising session types
- 2:29Extending projection in mechanisation
- 3:54Global types and projection
- 8:30Recursion and branching issues
- 12:00Coinductive projection definition
- 15:12Candidate projection validation
- 19:49Compliance check and equivalence
- 21:17Soundness and completeness
- 22:22Related work and mechanisation
- 24:51Q&A