Special Delivery: Programming with Mailbox Types
summary
Pat implements mailbox types that model each mailbox as a commutative regular expression and statically rule out protocol violations (double put, missing reply, payload mismatch, self-deadlock). The design uses quasi-linear typing to allow many senders but one guarded receiver and a backwards bidirectional typing algorithm that emits pattern-inclusion constraints solved (with a closed-form simplifier and Z3). A prototype type checker verifies Savina benchmarks in under 100 ms and a factory automation case study; soundness and completeness are proved.
AI-written summary · about
chapters (12)
- 0:00Mailbox types intro
- 2:28Actor model and mailbox
- 5:15Future example and errors
- 7:46Calculus to programming language
- 8:27Demo of Pat tool
- 10:18Language design challenges
- 12:03Quasi-linear typing
- 14:29Subtyping and semantics
- 16:57Algorithmic type system
- 20:51Evaluation and factory use case
- 22:18Summary and future work
- 23:23Q&A
related talks
14mLightning Talk: Towards Mailbox Typing for Erlang
20mImplementability of Global Distributed Protocols Modulo Network Architectures
20mMessage-Observing Sessions
39mProtocol engineering for communicating actors
20mModel Checking Distributed Protocols in Must
42mTime-sensitive protocol: Links From Design to Implementation
45mTaming Distribution: Formal Protocols for Akka Typed
15mStatically Verified Refinements for Multiparty Protocols