Message-Observing Sessions
summary
Most is a process language that adds message-observing session types — a restricted form of type-level computation — to binary session types so protocols on one channel can depend on messages seen on others, allowing bottom-up specifications of global invariants. Semantics uses traces with binding to model name generation; the authors give a recursive type-checking algorithm and prove type soundness and compositionality. Type checking is decidable but composition checking can blow up exponentially; no compiler or implementation yet.
AI-written summary · about
chapters (14)
- 0:00Message observing sessions
- 1:26Communication protocols
- 2:49Research question and session types
- 3:52Communicating systems and protocols
- 5:38Limitations of binary session types
- 6:22MOST language
- 7:47Type-level computation syntax and semantics
- 9:36Dependent protocols with MOST
- 10:40Compositional reasoning with assumptions
- 11:22Denotational semantics and trace sets
- 12:44Static type checking
- 13:47Correctness and comparisons
- 14:50Future work and challenges
- 15:38Q&A
related talks
23mA Synthetic Reconstruction of Multiparty Session Types
37mSession Types: A History and Applications
48mUnderstanding concurrency with behavioural types
31mSo what's the difference between a session type and an ordinary type anyway?
21mPolymorphic Typestate for Session Types
32mIntrinsically Typed Sessions with Callbacks
12mA Unified View of Modalities in Type Systems
15mStatically Verified Refinements for Multiparty Protocols