Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Fre...
summary
A functional language MPGV extends GV with multiparty session types, first-class channel endpoints, dynamic spawning and a new redirect construct that enables type-preserving translation from binary GV. Semantics are asynchronous with threads and buffers, mechanized in Coq: the development is ~500 lines of definitions and ~10,000 lines of proofs. The system proves session fidelity, deadlock freedom, and a one-line global progress corollary guaranteeing nontrivial safety for translated programs.
AI-written summary · about
chapters (7)
- 0:00Start
- 0:39Binary session types: Honda et al. '93, 98
- 1:52Multiparty session types: Honda et al.'08
- 2:31Two worlds of session types
- 9:51Mechanized metatheory
- 11:21How to know that you mechanized the right theorem?
- 12:54What's in the paper
related talks
15mBorrowing From Session Types
23mConnectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation L
01h 01mThe Future of Concurrency and Parallelism
25mA Logical Interpretation of Asynchronous Multiparty Compatibility
16mAutomated Verification of Parametric Channel-Based Process Communication
54mShared Session Types for Safe, Practical Concurrency
35mAsynchronous and Synchronous Mixed Sessions
20mDeadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-O...