Special Delivery: Programming with Mailbox Types (Extended Version)
Simon Fowler, Duncan Paul Attard, Danielle Marshall, Simon J. Gay, Phil Trinder

TL;DR
This paper introduces Pat, a novel programming language with mailbox types that detect communication errors in actor-based systems, enhancing reliability and safety in distributed programming.
Contribution
It presents the first implementation of mailbox types in a programming language, including a type system, algorithm, and practical case studies demonstrating its effectiveness.
Findings
Typechecking detects protocol violations, unexpected messages, forgotten replies, and self-deadlocks.
The type system is sound and complete, validated through case studies and benchmarks.
Pat demonstrates practical expressiveness for actor-based programming.
Abstract
The asynchronous and unidirectional communication model supported by mailboxes is a key reason for the success of actor languages like Erlang and Elixir for implementing reliable and scalable distributed systems. Although actors eliminate many of the issues stemming from shared memory concurrency, they remain vulnerable to communication errors such as protocol violations and deadlocks. Behavioural types make it possible to detect communication errors early in the development process, but most work has addressed channel-based languages rather than actor languages. Mailbox types are a novel behavioural type system for actors first introduced for a process calculus, and capture the contents of a mailbox as a commutative regular expression. Due to aliasing and nested evaluation contexts, moving from a process calculus to a programming language is challenging. This paper presents Pat, the…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Security and Verification in Computing
