Title: Mailbox Types for Unordered Interactions,
Abstract: We propose a type system for reasoning on protocol conformance and deadlock
freedom in networks of processes that communicate through unordered mailboxes.
We model these networks in the mailbox calculus, a mild extension of the
asynchronous {\pi}-calculus with first-class mailboxes and selective input. The
calculus subsumes the actor model and allows us to analyze networks with
dynamic topologies and varying number of processes possibly mixing different
concurrency abstractions. Well-typed processes are deadlock free and never fail
because of unexpected messages. For a non-trivial class of them, junk freedom
is also guaranteed. We illustrate the expressiveness of the calculus and of the
type system by encoding instances of non-uniform, concurrent objects, binary
sessions extended with joins and forks, and some known actor benchmarks.