Statically Verified Refinements for Multiparty Protocols
summary
Theory proves refined multiparty session types preserve trace equivalence while tracking variable knowledge with multiplicities 0 or ω; implementation builds a toolchain called Session that parses extended Scribble protocols with refinement annotations, generates F APIs, uses Z3-backed F* typechecking to statically verify refinements, and extracts verified code to OCaml. The runtime enforces linearity via a callback-style API, the example shows decision logic for Higher/Lower/Correct is statically rejected if comparisons are flipped, and the artifact ships as Docker + GitHub.
AI-written summary · about
chapters (12)
- 0:00Intro
- 0:16Multiparty Session Types (MPST) A typing discipline for message passing concurrency
- 3:13Refinement Types Refining base types with predicates
- 4:14Contribution
- 4:39Refined Multiparty Session Types (RMPST)
- 6:25Tracking Knowledge in Typing Contexts
- 7:58Semantics - Labelled Transition System
- 9:07Session* - A Toolchain for RMPST Workflow
- 10:05Specifying Protocols using the Scribble Protocol Description Language
- 10:35API Style
- 13:08Implementing Endpoints
- 14:19Future Work
related talks
23mA Synthetic Reconstruction of Multiparty Session Types
20mSift: Using Refinement-guided Automation to Verify Complex Distributed Systems
18mHybrid Multiparty Session Types: Compositionality for Protocol Specification th...
37mSession Types: A History and Applications
32mBenchmarks for Multiparty Session Types
14mA Refinement Methodology for Distributed Programs in Rust
35mEvent-Driven Multiparty Session Actors
32mMulticompatibility for Multiparty-Session Composition