Asynchronous and Synchronous Mixed Sessions
summary
Claim: binary session types with mixed choices (CMV+) do not increase synchronous expressiveness — neither for linear nor unrestricted channels — despite appearing to allow true mixed input/output choices. Proof uses a leader-election impossibility, a confluence-like lemma and the synchronization star is absent pattern to show no extra power, plus a correctness-preserving encoding back to non-mixed sessions. A careful asynchronous semantics with FIFO queues requires encoding choice roles into labels (naive queueing deadlocks), so mixed syntax adds flexibility but not new synchronous power.
AI-written summary · about
chapters (15)
- 0:00Mixed sync/async sessions intro
- 1:05P and session types calculus
- 3:16Mixed choice in calculus C
- 5:01Mixed choice expressive power
- 6:48Proving lack of expressive power increase
- 7:52Leader election analysis
- 13:04Leader election failures
- 18:26Confluence lemma proof
- 19:08Synchronization patterns
- 22:43Expressiveness findings summary
- 24:10Mixed sessions with queues
- 27:01Encoding via duality
- 29:07Async semantics with cues
- 31:56Syntax and semantics limits
- 33:05Q&A
related talks
25mA Logical Interpretation of Asynchronous Multiparty Compatibility
54mShared Session Types for Safe, Practical Concurrency
23mPrecise Subtyping for Asynchronous Multiparty Sessions
16mVerified Lock-Free Session Channels with Linking
36mConcurrent ML - The One That Got Away
50mSession Types Meet Polymorphism and Dependent Types
14mMultiparty GV: Functional Multiparty Session Types with Certified Deadlock Fre...
01h 35mThinking Outside the Synchronisation Quadrant