Precise Subtyping for Asynchronous Multiparty Sessions
summary
First formalization of precise subtyping for asynchronous multiparty sessions that proves both soundness (safe replacement) and completeness (no larger relation is safe). Uses a novel session decomposition into single input/output trees and two simple refinement rules that capture all safe input/output reorderings under FIFO queues. Builds characteristic processes and sessions to exhibit counterexamples when subtyping fails. Proves operational and denotational preciseness, gives subject reduction and type safety theorems, and the technique scales to recursive types.
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:55A Simple Motivating Example Consider a distributed computing system with participants p......
- 3:17Background: Subtyping for Communication Protocols Session types are types for protocols
- 4:57Background: Asynchronous Sessions
- 6:15Our Goal: Find the "Best" Subtyping for Asynchronous Sessions
- 7:49Formalism: a Streamlined Process Calculus with Session Types
- 9:07Formalism: What Errors we want to Avoid
- 9:51Key Insight and Novelty: Session Decomposition Challenge: cur asynchronous subtyping must subsume synchronous subtyping
- 14:01SISO refinement
- 15:30The First Definition of Asynchronous Multiparty Session Subtyping
- 17:52Result: Soundness of Asynchronous Session Subtyping
- 18:56Result: Completeness of Asynchronous Session Subtyping
- 20:50Main Result: Preciseness of Subtyping... in Multiple Flavours!
- 21:23Conclusion We presented the first formalisation
related talks
21mFair Termination of Binary Sessions
23mProbabilistic Refinement Session Types
50mSession Types Meet Polymorphism and Dependent Types
25mA Logical Interpretation of Asynchronous Multiparty Compatibility
54mShared Session Types for Safe, Practical Concurrency
35mAsynchronous and Synchronous Mixed Sessions
28mDependent Session Protocols in Separation Logic from First Principles
15mBorrowing From Session Types