We present a behavioral type system for reasoning on protocol conformance in networks of processes that communicate through unordered mailboxes. This communication model is the one adopted by concurrent objects and actors.

In sharp contrast with other behavioral types (session types in particular), the type of a mailbox specifies which patterns of messages are supposed to be stored in - or retrieved from - a mailbox, but not in which order. This allows the description of mailboxes concurrently accessed by several processes, abstracting away from the state and behavior of the processes using them.

There seem to be analogies between mailbox types and linear logic formulas, as well as between the typing rules and the proof rules of classical linear logic. With this seminar we seek to initiate a deeper investigation of these analogies.