A Logical Interpretation of Asynchronous Multiparty Compatibility
summary
Claims a syntactic, logical criterion that exactly captures asynchronous multiparty compatibility by encoding session types as linear propositions, using tensor=send par=receive and adding per-channel buffers. Types are annotated with sender/receiver labels to form buffer-labeled judgments, and the construction of asynchronous forwarders yields a decidable witness: if forwarders exist the processes are semantically compatible and their communications normalize. Work covers finite processes and shows forwarders compose; extending to infinite-state systems remains open.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:22Curry-Howard correspondence
- 1:06Session types and linear logic
- 3:38Multiparty compatibility
- 9:06Binary synchronous compatibility
- 10:34Extending to multiparty
- 13:42Asynchronous challenges
- 16:13Compatibility characterization
- 21:24Achievements and future work
- 22:07Q&A
related talks
35mAsynchronous and Synchronous Mixed Sessions
23mPrecise Subtyping for Asynchronous Multiparty Sessions
14mMultiparty GV: Functional Multiparty Session Types with Certified Deadlock Fre...
16mVerified Lock-Free Session Channels with Linking
36mConcurrent ML - The One That Got Away
31mTermination in Concurrency, Revisited
39mConcurrent Languages are Functional
50mSession Types Meet Polymorphism and Dependent Types