text:
\section{Concluding Remarks}
\label{sec:conclusions}

We have presented a mailbox type system for reasoning about
processes that communicate through first-class, unordered
mailboxes. The type system enforces mailbox conformance, deadlock
freedom and, for a significant class of processes, junk freedom as
well.
In sharp contrast with session types, mailbox types embody the
unordered nature of mailboxes and enable the description of
mailboxes concurrently accessed by several processes, abstracting
away from the state and behavior of the objects/actors/processes
using these mailboxes. The fact that a mailbox may have different
types during its lifetime is entirely encapsulated by the typing
rules and not apparent from mailbox types themselves.
The mailbox calculus subsumes the actor model and allows us to
analyze systems with a dynamic network topology and a varying number
of processes mixing different concurrency abstractions.

There are two natural extensions of the mailbox calculus that we
have not incorporated in the formal development for the sake of
simplicity.
First, it is possible to relax the syntax of guarded processes to
accommodate actions referring to different mailboxes as well as
actions representing timeouts. This extension makes the typing rules
for guards more complex to formulate but enhances expressiveness and
precision of typing (see Appendix~\ref{sec:example_readers_writer}).
Second, it is possible to allow multiple processes to receive
messages from the same mailbox by introducing a distinguished
capability that identifies shared mailboxes.  The notion of type
combination (Definition~\ref{def:type_combination}) must be suitably
revised for deadling with shared mailboxes and avoid the soundness
problems discussed in Example~\ref{ex:linear_input}.  With this
extension in place, it might also be possible to replace recursion
with replication in the calculus.

Concerning further developments, the intriguing analogies between
the mailbox type system and linear logic pointed out in
Section~\ref{sec:related} surely deserve a formal investigation.
On the practical side, a primary goal to fulfil is the development
of a type checking/inference algorithm for the proposed typing
discipline.  Subtyping is decidable and a type checking algorithm
for a slightly simpler type language has already been
developed~\cite{CobaltBlue}. We are confident that a type checking
algorithm for the mailbox calculus can be obtained by reusing much
of these known results.
Concerning the applicability of the approach to real-world
programming languages, one promising approach is the development of
a tool for the analysis of Java bytecode, possibly with the help of
Java annotations, along the lines of what has already been done for
Kilim~\cite{SrinivasanMycroft08}.
Other ideas for further developments include the extension of
pattern atoms so as to accommodate Erlang-style matching of messages
and the implementation of optimal matching algorithms driven by type
information.

\subsection{Actors using futures}
\label{sec:example_account_await}

Many Scala programs combine actors with
futures~\cite{TasharofiDingesJohnson13}.
As an example, Listing~\ref{lst:account_await} shows an alternative
version of the \lstinline[language=Scala,style=INLINE]{Account} actor in Akka that differes from
Listing~\ref{lst:account} in the handling of \lstinline[language=Scala,style=INLINE]{CreditMessages}
(lines~\ref{account.future.begin}--\ref{account.future.end}). The
\lstinline[language=Scala,style=INLINE]{future} variable created here is initialized asynchronously with
the result of the debit operation invoked on \lstinline[language=Scala,style=INLINE]{recipient}. To make
sure that each transaction is atomic, the actor waits for the
variable to be resolved (line~\ref{account.future.end}) before
notifying \lstinline[language=Scala,style=INLINE]{sender} that the operation has been completed.

This version of \lstinline[language=Scala,style=INLINE]{Account} is arguably simpler than the one in
Listing~\ref{lst:account}, if only because the actor has a unique
top-level behavior. One way of modeling this implementation of
\lstinline[language=Scala,style=INLINE]{Account} in the mailbox calculus is to use $\RecVar[Future]$,
discussed in Example~\ref{ex:future}.
A simpler modeling stems from the observation that \lstinline[language=Scala,style=INLINE]{future} in
Listing~\ref{lst:account_await} is used for a one-shot
synchronization.  A future variable with this property is akin to a
mailbox from which the value of the resolved variable is retrieved
exactly once. Following this approach we obtain the process below:
\[
  \begin{array}{@{}rcl@{}}
    \RecVar[Account](\Var[self], \Var[balance]) & \triangleq &
    \Receive\Var[self]\Tag[debit]{\Var[amount],\Var[sender]}
    \\ & &
    \Send\Var[sender]\Tag[reply]{}
    \mathbin\ttbar
    \invoke\RecVar[Account]{\Var[self], \Var[balance] + \Var[amount]}
    \\
    & + &
    \Receive\Var[self]\Tag[credit]{\Var[amount],\Var[recipient],\Var[sender]}
    \\ & &
    \New\Var[future]\bigparens{
      \begin{lines}
        \Send\Var[recipient]\Tag[debit]{\Var[amount],\Var[future]}
        \mathbin\ttbar {}
        \\
        \Receive\Var[future]\Tag[reply]{}
        \Free\Var[future]
        \\
        \parens{
          \Send\Var[sender]\Tag[reply]{}
          \mathbin\ttbar
          \invoke\RecVar[Account]{\Var[self], \Var[balance] + \Var[amount]}
        }
      \end{lines}
    }
    \\
    & + &
    \Receive\Var[self]\Tag[stop]{}
    \Free\Var[self]\mkkeyword{done}
    \\
    & + &
    \Receive\Var[self]\Tag[reply]{}
    \Fail\Var[self]
  \end{array}
\]

Compared to the process in Example~\ref{ex:account}, here the
notification from the $\Var[recipient]$ account is received from the
mailbox $\Var[future]$, which is created locally during the
handling of the $\Tag[credit]$ message. The rest of the process is the
same as before. This definition of $\RecVar[Account]$ and the one in
Example~\ref{ex:account} can both be shown to be consistent with the
declaration
\[
  \RecVar[Account] : (\Var[self] :
  \ttqmark\parens{
    \tmessage\Tag[debit]{\mkkeyword{int},\rho}^{\ast}
    \cdot
    \tmessage\Tag[credit]{\mkkeyword{int},\ttemark\tmessage\Tag[debit]{\mkkeyword{int},\rho},\rho}^{\ast}
    +
    \Tag[stop]}, \Var[balance] : \mkkeyword{int}; \emptyset)
\]
where $\rho \stackrel{\text{\tiny def}}= \ttemark\Tag[reply]$.  In particular, the
dependencies between $\Var[self]$ and $\Var[future]$ that originate
in this version of $\RecVar[Account]$ are not observable from outside
$\RecVar[Account]$ itself.

The use of multiple mailboxes and the interleaving of blocking
operations on them may increase the likelyhood of programming
mistakes causing mismatched communications and/or
deadlocks. However, these errors can be detected by a suitable
typing discipline such the one proposed in this paper.
Types can also be used to mitigate the runtime overhead resulting
from the use of multiple mailboxes. Here, for example, the typing of
$\Var[future]$ guarantees that this mailbox is used for receiving
a \emph{single} message and that $\Var[future]$ is empty by the
time $\Free[]\Var[future]$ is performed. A clever compiler can
take advantage of this information to statically optimize both the
allocation and the deallocation of this mailbox.

\subsection{Encoding of binary sessions}
\label{sec:example_binary_sessions}

\newcommand{\SessionProcess}[1]{\RecVar[Session]_{#1}}
\newcommand{\CreateSessionProcess}[1]{\RecVar[Create]_{#1}}
\newcommand{\EncodeSessionType}[1]{\mathcal{E}(#1)}
\newcommand{\Tag[op]}{\Tag[op]}

Session types~\cite{Honda93,HuttelEtAl16} have become a popular
formalism for the specification and enforcement of structured
protocols through static analysis.  A session is a private
communication channel shared by processes that interact through one
of its \emph{endpoint}. Each endpoint is associated with a
\emph{session type} that specifies the type, direction and order of
messages that are supposed to be exchanged through that endpoint. A
typical syntax for session types in the case of \emph{binary
  sessions} (those connecting exactly two peer processes) is shown
below:
\[
  T, S
  ~~::=~~
  \mkkeyword{end}
  ~~\mid~~
  \ttqmark\tmessage{}\tau.T
  ~~\mid~~
  \ttemark\tmessage{}\tau.T
  ~~\mid~~
  T \mathbin{\with} S
  ~~\mid~~
  T \mathbin{\oplus} S
\]

A session type $\ttqmark\tmessage{}\tau.T$ describes an
endpoint used for receiving a message of type $\tau$ and then
according to $T$.  Dually, a session type
$\ttemark\tmessage{}\tau.T$ describes an endpoint used for
sending a message of type $\tau$ and then according to
$T$.
An external choice $T \mathbin{\with} S$ describes
an endpoint used for receiving a selection (either $\Tag[left]$ or
$\Tag[right]$) and then according to the corresponding continuation
(either $T$ or $S$). Dually, an internal
choice $T \mathbin{\oplus} S$ describes an endpoint
used for making a selection and then according to the corresponding
continuation.
Communication safety and progress of a binary session are guaranteed
by the fact that its two endpoints are linear resources typed by
\emph{dual} session types, where the dual of $T$ is
obtained by swapping inputs with outputs and internal with external
choices.

In this example we encode sessions and session types using mailboxes
and mailbox types.  We encode a session as a non-uniform, concurrent
object. The object is ``concurrent'' because it is accessed
concurrently by the two peers of the session. It is ``non-uniform''
because its interface changes over time, as the session
progresses. The object uses a mailbox $\Var[self]$ and its behavior is
defined by the equations for $\SessionProcessT(\Var[self])$
shown below, where $T$ is the session type according to
which it must be used by one of the peers:
\[
  \begin{array}{@{}r@{~}c@{~}l@{}}
    \SessionProcess\mkkeyword{end}(\Var[self]) & \triangleq & \Free\Var[self]\mkkeyword{done}
    \\
    \SessionProcess{
      \ttqmark\tmessage{}\tau.T
    }(\Var[self]) & \triangleq &
    \Receive\Var[self]\Tag[send]{x,s}
    \Receive\Var[self]\Tag[receive]{r}
    \\ & &
    \parens{
      \Send{s}\Tag[reply]{x,\Var[self]}
      \mathbin\ttbar
      \Send{r}\Tag[reply]\Var[self]
      \mathbin\ttbar
      \invoke{\SessionProcessT}\Var[self]
    }
    \\
    \SessionProcess{\ttemark\tmessage{}\tau.T}(\Var[self]) & \triangleq &
    \invoke{\SessionProcess{\ttqmark\tmessage{}\tau.T}}\Var[self]
    \\
    \SessionProcess{T \mathbin{\with} S}(\Var[self]) & \triangleq &
    \Receive\Var[self]\Tag[left]{s}
    \Receive\Var[self]\Tag[receive]{r}
    \\ & &
    \parens{
      \Send{s}\Tag[reply]\Var[self]
      \mathbin\ttbar
      \Send{r}\Tag[left]\Var[self]
      \mathbin\ttbar
      \invoke{\SessionProcessT}\Var[self]
    }
    \\ & + &
    \Receive\Var[self]\Tag[right]{s}
    \Receive\Var[self]\Tag[receive]{r}
    \\ & &
    \parens{
      \Send{s}\Tag[reply]\Var[self]
      \mathbin\ttbar
      \Send{r}\Tag[right]\Var[self]
      \mathbin\ttbar
      \invoke{\SessionProcessS}\Var[self]
    }
    \\
    \SessionProcess{T \mathbin{\oplus} S}(\Var[self]) & \triangleq &
    \invoke{\SessionProcess{T \mathbin{\with} S}}\Var[self]
  \end{array}
\]

To grasp the intuition behind the definition of
$\SessionProcessT(\Var[self])$, it helps to recall that
each stage of a session corresponds to an interaction between the
two peers, where one process plays the role of ``sender'' and its
peer that of ``receiver''. Both peers manifest their willingness to
interact by storing a message into the session's mailbox. The
receiver always stores a $\Tag[receive]$ message, while the sender
stores either $\Tag[send]$, $\Tag[left]$ or $\Tag[right]$ according to
$T$. All messages contain a reference to the mailbox
owned by sender and receiver (respectively $s$ and $r$) where they
will be notified once the interaction is completed. A $\Tag[send]$
message also carries actual payload $\Var$ being exchanged. The role
of $\SessionProcessT(\Var[self])$ is simply to forward each
message from the sender to the receiver. The notifications stored in
$s$ and $r$ contain a reference to the session's mailbox so that its
type reflects the session's updated interface corresponding to the
rest of the conversation.

Interestingly, the encoding of a session with type $T$ is
undistinguishable from that of a session with the dual type
$\coT$. This is natural by recalling that each stage of a
session corresponds to a single interaction between the two peers:
the order in which they store the respective messages in the
session's mailbox is in general unpredictable but also unimportant,
for both messages are necessary to complete each interaction.

\newcommand{\RecVar[Alice]}{\RecVar[Alice]}
\newcommand{\RecVar[Carol]}{\RecVar[Carol]}

As an example, suppose we want to model a system where $\RecVar[Alice]$
asks $\RecVar[Carol]$ to compute the sum of two numbers exchanged through
a session $s$. $\RecVar[Alice]$ and $\RecVar[Carol]$ use the session according
to the session types
$T \stackrel{\text{\tiny def}}=
\ttemark\tmessage{}\mkkeyword{int}.\ttemark\tmessage{}\mkkeyword{int}.\ttqmark\tmessage{}\mkkeyword{int}.\mkkeyword{end}$
and
$\coT \stackrel{\text{\tiny def}}=
\ttqmark\tmessage{}\mkkeyword{int}.\ttqmark\tmessage{}\mkkeyword{int}.\ttemark\tmessage{}\mkkeyword{int}.\mkkeyword{end}$,
respectively.
The system is modeled as the process
\begin{equation}
  \label{eq:session}
  \New\Var[alice]
  \New\Var[carol]
  \New{s}\parens{
    \invoke\RecVar[Alice]{\Var[alice],s}
    \mathbin\ttbar
    \invoke\RecVar[Carol]{\Var[carol],s}
    \mathbin\ttbar
    \invoke{\SessionProcessT}{s}
  }
\end{equation}
where $\RecVar[Alice]$ and $\RecVar[Carol]$ are defined as follows:
\[
  \begin{array}{@{}r@{~}c@{~}l@{}}
    \RecVar[Alice](\Var[self],s) & \triangleq &
    \phantom(
    \Send{s}\Tag[send]{4,\Var[self]}
    \mathbin\ttbar
    \Receive\Var[self]\Tag[reply]{s}
    \\ & &
    \parens{
      \Send{s}\Tag[send]{2,\Var[self]}
      \mathbin\ttbar
      \Receive\Var[self]\Tag[reply]{s}
      \\ & &
      \parens{
        \Send{s}\Tag[receive]\Var[self]
        \mathbin\ttbar
        \Receive\Var[self]\Tag[reply]{\Var,s}
        \\ & &
        \parens{
          \Send\mathit{system}\Tag[print\ttunderscore int]\Var
          \mathbin\ttbar
          \Free\Var[self]
          \mkkeyword{done}
        }
      }
    }
    \\
    \RecVar[Carol](\Var[self],s) & \triangleq &
    \phantom(
    \Send{s}\Tag[receive]\Var[self]
    \mathbin\ttbar
    \Receive\Var[self]\Tag[reply]{\Var[x],s}
    \\ & &
    \parens{
      \Send{s}\Tag[receive]\Var[self]
      \mathbin\ttbar
      \Receive\Var[self]\Tag[reply]{\Var[y],s}
      \\ & &
      \parens{
        \Send{s}\Tag[send]{\Var[x] + \Var[y], \Var[self]}
        \mathbin\ttbar
        \Receive\Var[self]\Tag[reply]{s}
        \Free\Var[self]
        \mkkeyword{done}
      }
    }
  \end{array}
\]

The process~\eqref{eq:session} and the definitions of $\RecVar[Alice]$
and $\RecVar[Carol]$ are well typed.  In general,
$\SessionProcessT$ is consistent with the declaration
$\SessionProcessT : (\Var[self] :
\ttqmark(\EncodeSessionTypeT \cdot
\EncodeSessionType{\coT}); \emptyset)$ where
$\EncodeSessionTypeT$ is the pattern defined by the
following equations:
\[
  \begin{array}[b]{@{}r@{~}c@{~}l@{}}
    \EncodeSessionType\mkkeyword{end} & \stackrel{\text{\tiny def}}= & \mathbb{1}
    \\
    \EncodeSessionType{\ttqmark\tmessage{}\tau.T} & \stackrel{\text{\tiny def}}= &
    \tmessage\Tag[receive]{\ttemark\tmessage\Tag[reply]{\tau,\ttemark\EncodeSessionTypeT}}
    \\
    \EncodeSessionType{\ttemark\tmessage{}\tau.T} & \stackrel{\text{\tiny def}}= &
    \tmessage\Tag[send]{\tau,\ttemark\tmessage\Tag[reply]{\ttemark\EncodeSessionTypeT}}
    \\
    \EncodeSessionType{T \mathbin{\with} S} & \stackrel{\text{\tiny def}}= &
    \tmessage\Tag[receive]{\ttemark\parens{
        \tmessage\Tag[left]{\ttemark\EncodeSessionTypeT}
        +
        \tmessage\Tag[right]{\ttemark\EncodeSessionTypeS}
      }
    }
    \\
    \EncodeSessionType{T \mathbin{\oplus} S} & \stackrel{\text{\tiny def}}= &
    \tmessage\Tag[left]{\ttemark\tmessage\Tag[reply]{\ttemark\EncodeSessionTypeT}}
    +
    \tmessage\Tag[right]{\ttemark\tmessage\Tag[reply]{\ttemark\EncodeSessionTypeS}}
  \end{array}
\]

This encoding of binary sessions extends easily to internal and
external choices with arbitrary labels and also to recursive session
types by interpreting both the syntax of $T$ and the
definition of $\SessionProcessT$ coinductively. The usual
regularity condition ensures that $\SessionProcessT$ is
finitely representable. Finally, note that the notion of subtyping
for encoded session types induced by Definition~\ref{def:subt}
coincides with the conventional one~\cite{GayHole05}. Thus, the
mailbox type system subsumes a rich session type system where
Theorem~\ref{thm:soundness} corresponds to the well-known
communication safety and progress properties of sessions.

\subsection{Type-safe mailbox downcast}
\label{sec:example_downcast}

\newcommand{\Var[Cast]}{\Var[Cast]}
\newcommand{\Tag[cast]}{\Tag[cast]}

\[
  \begin{array}{@{}r@{~}c@{~}l@{}}
    \Var[Cast](\Var[self]) & \triangleq &
    \Receive\Var[self]\Tag[cast]{\Var[x],\Var[y]}
    \\
    & &
    (\Receive\Var[x]\Tag[A]{}(\Send\Var[x]\Tag[A]{} \mathbin\ttbar \Send\Var[y]\Tag[A]\Var[x])
    +
    \Receive\Var[x]\Tag[B]{}(\Send\Var[x]\Tag[B]{} \mathbin\ttbar \Send\Var[y]\Tag[B]\Var[x]))
  \end{array}
\]

\subsection{Encoding of sessions with forks and joins}
\label{sec:example_forks_joins}

\newcommand{\Tag[Then]}{\Tag[Then]}
\newcommand{\CollectProcess}[1]{\RecVar[Join]_{#1}}

We have seen that it is possible to share the output capability on a
mailbox among several processes. We can take advantage of this
feature to extend session types with forks and joins:
\[
  T, S
  ~~::=~~
  \mkkeyword{end}
  ~~\mid~~
  \ttqmark\tmessage{}\tau.T
  ~~\mid~~
  \ttemark\tmessage{}\tau.T
  ~~\mid~~
  T \mathbin{\with} S
  ~~\mid~~
  T \mathbin{\oplus} S
  ~~\mid~~
  {\parr}_{i\in I} \tmessage{\Tag_i}{\tau_i};T
  ~~\mid~~
  {\otimes}_{i\in I} \tmessage{\Tag_i}{\tau_i};T
\]

The idea is that the session type
${\otimes}_{1\leq i\leq n} \tmessage{\Tag_i}{\tau_i};T$
describes an endpoint that can be used for sending \emph{all} of the
$\Tag_i$ messages, and then according to $T$. The
difference between
${\otimes}_{1\leq i\leq n} \tmessage{\Tag_i}{\tau_i};T$ and
a session type of the form
$\ttemark\tmessage{}{\tau_1}\dots\ttemark\tmessage{}{\tau_n}.T$
is that the $\Tag_i$ messages can be sent by independent processes
(for example, by parallel workers) in whatever order instead of by a
single sender.
Dually, the session type
${\parr}_{1\leq i\leq n} \tmessage{\Tag_i}{\tau_i};T$
describes an endpoint that can be used for collecting \emph{all} of
the $\Tag_i$ messages, and then according to $T$.
Forks and joins are dual to each other, just like simple outputs are
dual to simple inputs. The tags $\Tag_i$ need not be distinct, but
equal tags must correspond to equal argument types.

The extension of $\SessionProcessT$ to forks and joins is
shown below:
\[
  \begin{array}{@{}r@{~}c@{~}l@{}}
    \SessionProcess{
      {\otimes}_{i\in I} \tmessage{\Tag_i}{\tau_i};T
    }(\Var[self]) & \triangleq &
    \Receive\Var[self]\Tag[send]{s}
    \Receive\Var[self]\Tag[receive]{r}
    \invoke{
      \CollectProcess{
        {\otimes}_{i\in I} \tmessage{\Tag_i}{\tau_i};T
      }
    }{\Var[self],s,r}
    \\
    \SessionProcess{
      {\parr}_{i\in I} \tmessage{\Tag_i}{\tau_i};T
    }(\Var[self]) & \triangleq &
    \invoke{
      \SessionProcess{
        {\otimes}_{i\in I} \tmessage{\Tag_i}{\tau_i};T
      }
    }{\Var[self]}
    \\
    \CollectProcess{
      {\otimes}_{i\in I} \tmessage{\Tag_i}{\tau_i};T
    }(\Var[self],s,r) & \triangleq &
    \begin{cases}
      \Send{s}\Tag[reply]\Var[self]
      \mathbin\ttbar
      \Send{r}\Tag[reply]\Var[self]
      \mathbin\ttbar
      \invoke{\SessionProcessT}\Var[self]
      & \text{if $I = \emptyset$}
      \\
      \Receive\Var[self]{\Tag_i}{\Var_i}\parens{
        \Send{r}{\Tag_i}{\Var_i}
        \mathbin\ttbar
        \invoke{
          \CollectProcess{
            {\otimes}_{i\in I\setminus\set{i}} \tmessage{\Tag_i}{\tau_i};T
          }
        }{\Var[self],s,r}
      }
      & \text{if $i \in I$}
    \end{cases}
    \\
    \SessionProcess{
      {\parr}_{i\in I} \tmessage{\Tag_i}{\tau_i};T
    }(\Var[self]) & \triangleq &
    \invoke{
      \SessionProcess{
        {\otimes}_{i\in I} \tmessage{\Tag_i}{\tau_i};T
      }
    }\Var[self]
  \end{array}
\]

As in the case of simple interactions, sender and receiver manifest
their willingness to interact by storing $\Tag[send]$ and
$\Tag[receive]$ messages into the session's mailbox $\Var[self]$. At
that point, $\invoke{\CollectProcessT}{\Var[self],s,r}$
forwards all the $\Tag_i$ messages coming from the sender side to
the receiver side, in some arbitrary order (case $i \in I$).
When there are no more messages to forward (case $I = \emptyset$)
both sender and receiver are notified with a $\Tag[reply]$ message
that carries a reference to the session's endpoint, with its type
updated according to the rest of the continuation.

The encoding of session types extended to forks and joins follows
easily:
\[
  \begin{array}{@{}r@{~}c@{~}l@{}}
    \EncodeSessionType{{\otimes}_{i\in I} \tmessage{\Tag_i}{\tau_i};T}
    & \stackrel{\text{\tiny def}}= &
    \tmessage\Tag[send]{\ttemark\tmessage\Tag[reply]{\ttemark\EncodeSessionTypeT}}
    \cdot
    \prod_{i\in I}
    \tmessage{\Tag_i}{\tau_i}
    \\
    \EncodeSessionType{{\parr}_{i\in I} \tmessage{\Tag_i}{\tau_i};T}
    & \stackrel{\text{\tiny def}}= &
    \tmessage\Tag[receive]{
      \ttemark
      \parens{
        \prod_{i\in I}
        \tmessage{\Tag_i}{\tau_i}
      }
      \cdot
      \tmessage\Tag[reply]{\ttemark\EncodeSessionTypeT}
    }
  \end{array}
\]

An alternative definition of $\CollectProcessT$ that
fowards messages as soon as they become available can be obtained by
providing suitable input actions for each $i\in I$ instead of
picking an arbitrary $i\in I$.

\subsection{Master-workers parallelism}
\label{sec:example_master_workers}

\newcommand{\RecVar[Available]}{\RecVar[Available]}
\newcommand{\RecVar[Worker]}{\RecVar[Worker]}
\newcommand{\RecVar[CreatePool]}{\RecVar[CreatePool]}
\newcommand{\RecVar[CollectResults]}{\RecVar[CollectResults]}
\newcommand{\Var[worker]}{\Var[worker]}
\newcommand{\Tag[task]}{\Tag[task]}
\newcommand{\Tag[work]}{\Tag[work]}
\newcommand{\Tag[one]}{\Tag[one]}

In this example we model a \emph{master} process that receives tasks
to perform from a \emph{client}. For each task, the master creates a
pool of \emph{workers} and assigns each worker a share of work.  The
master waits for all partial results from the workers before sending
the final result back to the client and making itself available
again.
The number of workers may depend on some quantity possibly related
to the task to be performed and that is known at runtime only.

Below we define three processes corresponding to the three states in
which the master process can be, and we leave $\RecVar[Worker]$
unspecified:
\[
  \begin{array}{@{}r@{~}c@{~}l@{}}
    \RecVar[Available](\Var[self]) & \triangleq &
    \Receive\Var[self]\Tag[task]\Var[client]
    \New\Var[pool]\invoke\RecVar[CreatePool]{\Var[self],\Var[pool],\Var[client]}
    \\
    & + & \Free\Var[self]\mkkeyword{done}
    \\
    \RecVar[CreatePool](\Var[self],\Var[pool],\Var[client]) & \triangleq &
    \IfX{~\textit{more workers needed}~}{
      \\ & & \quad
      \New\Var[worker](
      \Send\Var[worker]\Tag[work]\Var[pool]
      \mathbin\ttbar
      \invoke\RecVar[Worker]\Var[worker])
      \mathbin\ttbar
      {}
      \\ & & \quad
      \invoke\RecVar[CreatePool]{\Var[self],\Var[pool],\Var[client]}
      \\ & &
    }{
      \\ & & \quad
      \invoke\RecVar[CollectResults]{\Var[self], \Var[pool], \Var[client]}
    }
    \\
    \RecVar[CollectResults](\Var[self],\Var[pool],\Var[client]) & \triangleq &
    \Receive\Var[pool]\Tag[result]{}
    \invoke\RecVar[CollectResults]{\Var[self],\Var[pool],\Var[client]}
    \\
    & + &
    \Free\Var[pool]\parens{
      \Send\Var[client]\Tag[result]{}
      \mathbin\ttbar
      \invoke\RecVar[Available]\Var[self]
    }
  \end{array}
\]

The ``$\If{\mathit{condition}}PQ$'' form used here
can be encoded in the mailbox calculus and is typed similarly to the
non-deterministic choice of Example~\ref{ex:choice}.
These definitions can be shown to be consistent with the following
declarations:
\[
  \begin{array}{@{}r@{~}c@{~}l@{}}
    \RecVar[Available] & : & (\Var[self] : \ttqmark\tmessage\Tag[task]{\ttemark\Tag[result]}^{\ast}; \emptyset)
    \\
    \RecVar[CreatePool], \RecVar[CollectResults] & : & (\Var[self] : \ttqmark\tmessage\Tag[task]{\ttemark\Tag[result]}^{\ast},
    \Var[pool] : \ttqmark\Tag[result]^{\ast}, \Var[client] : \ttemark\Tag[result];
    \\
    & & \phantom{(}
    \gedge\Var[pool]\Var[self] \sqcup \gedge\Var[pool]\Var[client])
  \end{array}
\]

The usual implementation of this coordination pattern requires the
programmer to keep track of the number of active workers using a
counter that is decremented each time a partial result is
collected~\cite{ImamSarkar14}. When the counter reaches zero, the
master knows that all the workers have finished their job and
notifies the client. In the mailbox calculus, we achieve the same
goal by means of a dedicated mailbox $\Var[pool]$ from which the
partial results are collected: when $\Var[pool]$ becomes disposable,
it means that no more active workers remain.\Luca{Questo esempio
  potrebbe essere criticato in quanto l'azione $\Free[]{}$ sembra
  implicare l'uso di un complesso garbage collector distribuito. Il
  garbage collector pu\`o essere realizzato in maniera efficiente,
  ma \`e difficile da spiegare e dunque poco convincente. Questo \`e
  anche l'unico esempio in cui $\Free[]{}$ \`e seguita da un'azione
  interessante e non da $\mkkeyword{done}$. Usando una sola mailbox si ricade
  nel problema del type pollution.}

\subsection{Parallel QuickSort}
\label{sec:example_quicksort}

\newcommand{\RecVar[QuickSort]}{\RecVar[QuickSort]}

The QuickSort algorithm lends itself naturally to a parallel
implementation, whereby the left and right partitions of a
sufficiently large collection of items can be sorted in
parallel. Below we see a modeling of the algorithm in the mailbox
calculus, where we have abstracted away any reference to the data
and focused exclusively on the communication structure:
\[
  \begin{array}{@{}r@{~}c@{~}l@{}}
    \RecVar[QuickSort](\Var[self]) & \triangleq &
    \Receive\Var[self]\Tag[sort]\Var[client]
    \\ & &
    \IfX{~\textit{data is small}~}{~
      \Send\Var[client]\Tag[result]{}
    ~}{
      \\ & & \quad
      \New\Var[l]
      \New\Var[r]\bigparens{
        \begin{lines}
          \New\Var[left]\parens{
            \Send\Var[left]\Tag[sort]\Var[l]
            \mathbin\ttbar
            \invoke\RecVar[QuickSort]\Var[left]
          }~\mathbin\ttbar
          \\
          \New\Var[right]\parens{
            \Send\Var[right]\Tag[sort]\Var[r]
            \mathbin\ttbar
            \invoke\RecVar[QuickSort]\Var[right]
          }~\mathbin\ttbar
          \\
          \Receive\Var[l]\Tag[result]{}
          \Free\Var[l]
          \Receive\Var[r]\Tag[result]{}
          \Free\Var[r]
          \\
          \parens{
            \Send\Var[client]\Tag[result]{}
            \mathbin\ttbar
            \invoke\RecVar[QuickSort]\Var[self]
          }
        \end{lines}
      }
    }
    \\ & + & \Free\Var[self]\mkkeyword{done}
  \end{array}
\]

The $\RecVar[QuickSort]$ process waits for $\Tag[sort]$ requests carrying a
reference to a mailbox $\Var[client]$ where the result is expected.
If the data to sort is small enough, the result is computed
sequentially. Otherwise, two new instances of $\RecVar[QuickSort]$ and
corresponding mailboxes $\Var[left]$ and $\Var[right]$ are created. The
partitioned data is assigned to the new processes via two $\Tag[sort]$
messages, each carrying a reference to a local mailbox for
collecting the results. Once the results have been collected, the
main process notifies $\Var[client]$ and makes itself available again.
The ``$\If{\mathit{condition}}PQ$'' form used here
can be encoded in the mailbox calculus and is typed similarly to the
non-deterministic choice of Example~\ref{ex:choice}.
The definition of $\RecVar[QuickSort]$ is well typed and consistent with
the declaration
$\RecVar[QuickSort] : (\Var[self] :
\ttqmark\tmessage\Tag[sort]{\ttemark\Tag[result]}^{\ast}; \emptyset)$.

Compared to a typical implementation of parallel QuickSort in the
actor model,\footnote{See for example the version included in the
  \texttt{Savina} benchmark suite~\cite{ImamSarkar14}.}  the use of
dedicated mailboxes $\Var[l]$ and $\Var[r]$ for
collecting the partial results from the two recursive invocations of
$\RecVar[QuickSort]$ has a beneficial impact.
In the pure actor model, the partial results are expected to be
found in $\Var[self]$, the only mailbox available to the parent actor.
This forced choice complicates the realization of the algorithm in
two ways.
First, each partial result from a recursive invocation must be
appropriately tagged so that the parent actor knows whether it
refers to the left or right partition of the collection being
sorted. Without this information, the parent actor would have to
peek inside the partial result to determine the order in which it
must be concatenated.
Most importantly, the natural control flow of the algorithm is
disrupted by the flat structure imposed by the actor model, which
requires the parent actor to handle both $\Tag[sort]$ and $\Tag[result]$
messages at the top-level. This forces the programmer to explicilty
write bookkeeping code in order to detect when all partial results
have been collected so that the client can be notified.
On the other hand, the availability of multiple mailboxes and the
interleaving of blocking operations on them may increase the
likelyhood of programming mistakes causing mismatched communications
and/or deadlocks. However, these errors can be detected by a
suitable typing discipline such the one proposed in this paper.
Types can also be used to mitigate the runtime overhead resulting
from the use of multiple mailboxes. Here, for example, the typing of
$\Var[l]$ and $\Var[r]$ guarantees that these
mailboxes are used for receiving a \emph{single} message and are
empty by the time $\Free[]\Var[l]$ and
$\Free[]\Var[r]$ are performed. A clever compiler can take
advantage of this information to statically optimize both the
allocation and the deallocation of these mailboxes.

\section{Readers-Writer Lock}
\label{sec:example_readers_writer}

\newcommand{\RecVar[Free]}{\RecVar[Free]}
\newcommand{\RecVar[Write]}{\RecVar[Write]}
\newcommand{\RecVar[Read]}{\RecVar[Read]}
\newcommand{\Var[w]}{\Var[w]}
\newcommand{\Var[r]}{\Var[r]}
\newcommand{\Tag[acquireW]}{\Tag[acquireW]}
\newcommand{\Tag[acquireR]}{\Tag[acquireR]}
\newcommand{\Tag[read]}{\Tag[read]}
\newcommand{\Tag[write]}{\Tag[write]}

A readers-writer lock grants read-only access to an arbitrary number
of readers and exclusive write access to a single writer. Below is a
particular modeling of a readers-writer lock making use of
\emph{mixed guards}, where different actions may refer to different
mailboxes:
\[
  \begin{array}{@{}r@{~}c@{~}l@{}}
    \RecVar[Free](\Var[self]) & \triangleq &
    \Free\Var[self]\mkkeyword{done}
    \\ & + &
    \Receive\Var[self]\Tag[acquireW]\Var[w]\parens{
      \Send\Var[w]\Tag[reply]\Var[self]
      \mathbin\ttbar
      \invoke\RecVar[Write]\Var[self]
    }
    \\ & + &
    \Receive\Var[self]\Tag[acquireR]\Var[r]
    \New\Var[pool]\parens{
      \Send\Var[r]\Tag[reply]\Var[pool]
      \mathbin\ttbar
      \invoke\RecVar[Read]{\Var[self],\Var[pool]}
    }
    \\ & + &
    \Receive\Var[self]\Tag[read]{}
    \Fail\Var[self]
    \\ & + &
    \Receive\Var[self]\Tag[write]\Var[w]
    \Fail\Var[self]
    \\
    \RecVar[Write](\Var[self]) & \triangleq &
    \Receive\Var[self]\Tag[release]{}
    \invoke\RecVar[Free]\Var[self]
    \\ & + &
    \Receive\Var[self]\Tag[write]\Var[w]\parens{
      \Send\Var[w]\Tag[reply]\Var[self]
      \mathbin\ttbar
      \invoke\RecVar[Write]\Var[self]
    }
    \\ & + &
    \Receive\Var[self]\Tag[read]{}
    \Fail\Var[self]
    \\
    \RecVar[Read](\Var[self],\Var[pool]) & \triangleq &
    \Receive\Var[self]\Tag[acquireR]\Var[r]\parens{
      \Send\Var[r]\Tag[reply]\Var[pool]
      \mathbin\ttbar
      \invoke\RecVar[Read]{\Var[self],\Var[pool]}
    }
    \\ & + &
    \Receive\Var[self]\Tag[write]\Var[w]
    \Fail\Var[self]
    \\ & + &
    \Receive\Var[pool]\Tag[read]{}
    \invoke\RecVar[Read]{\Var[self],\Var[pool]}
    \\ & + &
    \Free\Var[pool]\invoke\RecVar[Free]\Var[self]
  \end{array}
\]

The readers-writer lock may be free, in which case it can be
acquired either by a reader or by a writer but it does not accept
read or write requests. When the lock has been acquired by a writer
process, the writer is granted exclusive access and read requests
are not accepted. When a reader acquires a free lock, the lock
creates $\Var[pool]$ of readers and moves into a state where more
readers may be granted access. Each reader manifests its intention
to read the resource by storing a $\Tag[read]$ message into $\Var[pool]$
whereas prospective readers manifest their intention of accessing
the resource by storing $\Tag[acquireR]$ into $\Var[self]$. The
mixed guard in the $\RecVar[Read]$ process is key to serve both kinds of
requests. In particular, when all readers have terminated,
$\Var[pool]$ can be deleted and the lock moves back into the free
state.

\begin{table}
  \begin{center}
    \[
      \begin{array}{@{}c@{}}
        \inferrule{
          \wtg{
            \seqof\NameU : \ttqmark\seqof\Pattern,
            \Gamma;
            \seqof\NameU : \ttqmark\seqof\Pattern
          }{
            G
          }
          \\
          \vDash \seqof\Pattern
        }{
          \textstyle
          \wtp{
            \seqof\NameU : \ttqmark\seqof\Pattern,
            \Gamma
          }{
            G
          }{
            \gedge{\set\seqof\NameU}{\mathsf{dom}(\Gamma)}
          }
        }
        ~~\defrule{t-guard*}
        \\\\
        \inferrule{

        }{
          \wtg{
            \Gamma;
            u : \ttqmark\mathbb{0}
          }{
            \Failu
          }
        }
        ~~\defrule{t-fail*}
        \qquad
        \inferrule{
          \wtp\ContextAP\varphi
        }{
          \wtg{
            u : \tau, \Gamma;
            u : \ttqmark\mathbb{1}
          }{
            \FreeuP
          }
        }
        ~~\defrule{t-free*}
        \\\\
        \inferrule{
          \wtp{
            u : \ttqmarkE,
            \Gamma,
            \seqof\VarX : \seqof\Type
          }{
            P
          }{
            \varphi
          }

        }{
          \wtg{
            u : \tau, \Gamma;
            u : \ttqmark(\tmessage\Tag\seqof\Type\tmulE)
          }{
            \Receiveu\Tag\seqof\VarXP
          }
        }
        ~~\defrule{t-in*}
        \qquad
        \inferrule{
          \wtg{
            \Gamma;
            \Delta_i
          }{
            G_i
          }
          ~{}^{(i=1,2)}
        }{
          \wtg{
            \Gamma;
            \Delta_1 + \Delta_2
          }{
            G_1 + G_2
          }
        }
        ~~\defrule{t-branch*}
      \end{array}
    \]
  \end{center}
  \caption{
    \label{tab:relaxed_typing} Relaxed typing rules for mixed guards.
  }
\end{table}

In order to deal with mixed guards, the typing rules for guards and
guarded processes must be generalized as shown in
Table~\ref{tab:relaxed_typing}. The basic idea is the same as for
restricted guards, namely the type of mailboxes different from the
one referred to by an action cannot be affected by the content (or
lack thereof) of that mailbox. To do so, the judgments for guards
have the form $\wtg{\Gamma;\Delta}G$ where $\Gamma$ is
the type environment of the guarded process as a whole whereas
$\Delta$ keeps track of the types of the mailboxes referred to by
the actions, which are split exactly as in the restricted typing
rules (Table~\ref{tab:inference}). The $+$ operation on type
environments is defined thus:
\[
  \Gamma_1 + \Gamma_2 =
  \begin{cases}
    \Gamma_1, \Gamma_2 & \text{if
      $\mathsf{dom}(\Gamma_1) \cap \mathsf{dom}(\Gamma_2) = \emptyset$}
    \\
    u : \ttqmark(E_1 + E_2), \Gamma_1' +
    \Gamma_2' & \text{if
      $\Gamma_1 = u : \ttqmarkE_1, \Gamma_1'$ and
      $\Gamma_2 = u : \ttqmarkE_2, \Gamma_2'$}
  \end{cases}
\]

With the relaxed rules, it is possible to show that the above
process definitions are consistent with the following declarations
\[
  \begin{array}{@{}r@{~}c@{~}l@{}}
    \RecVar[Free] & : &
    \parens{
      \Var[self] : \ttqmark\parens{
        \tmessage\Tag[acquireW]\tau^{\ast}
        \cdot
        \tmessage\Tag[acquireR]\rho^{\ast}
      };
      \emptyset
    }
    \\
    \RecVar[Write] & : &
    \parens{
      \Var[self] : \ttqmark\parens{
        \tmessage\Tag[acquireW]\tau^{\ast}
        \cdot
        \tmessage\Tag[acquireR]\rho^{\ast}
        \cdot
        \parens{
          \Tag[release]
          +
          \tmessage\Tag[write]\tau
        }
      };
      \emptyset
    }
    \\
    \RecVar[Read] & : &
    \parens{
      \Var[self] : \ttqmark\parens{
        \tmessage\Tag[acquireW]\tau^{\ast}
        \cdot
        \tmessage\Tag[acquireR]\rho^{\ast}
      },
      \Var[pool] : \ttqmark\Tag[read]^{\ast};
      \gedge\Var[self]\Var[pool]
    }
  \end{array}
\]
where
$\tau \stackrel{\text{\tiny def}}= \ttemark\tmessage\Tag[reply]{ \ttemark\parens{ \Tag[release]
    + \tmessage\Tag[write]\tau } }$ and
$\rho = \ttemark\tmessage\Tag[reply]{ \ttemark\Tag[read]^{\ast} }$.
The remarkable aspect of this typing is that it guarantees
statically the key properties of the readers-writer lock: that there
are no readers nor writers when the lock is free; that there are no
readers if there is a single writer; that there is no writer if
there are one or more readers. Once again, the modeling makes key
use of multiple mailboxes so as to keep the typing as precise as
possible.

\section{Examples}
\label{sec:examples}

In this section we discuss a few more examples that illustrate the
expressiveness of the mailbox calculus and of its type system. We
consider a variant of the bank account shown in
Listing~\ref{lst:account} (Section~\ref{sec:example_account_await}),
the case of master-workers parallelism
(Section~\ref{sec:example_master_workers}) and the encoding of
binary sessions extended with forks and joins
(Sections~\ref{sec:example_binary_sessions}
and~\ref{sec:example_forks_joins}).

\input{example_account_await}
\input{example_master_workers}
\input{example_binary_sessions}
\input{example_forks_joins}

\section{Supplementary Properties}
\label{sec:extra_properties}

\input{prop_subtyping}
\input{prop_graphs}
\input{prop_type_environments}

\subsection{Dependency Graphs}
\label{sec:graphs}

We use \emph{dependency graphs} for tracking dependencies between
mailboxes. Intuitively, there is a dependency between $u$ and
$v$ if either $v$ is the argument of a message in mailbox
$u$ or $v$ occurs in the continuation of a process waiting
for a message from $u$.
Dependency graphs have names as vertices and undirected
edges. However, the usual representation of graphs does not account
for the fact that mailbox names may be restricted and that the
multiplicity of dependencies matters. Therefore, we define
dependency graphs using the syntax below:
\[
  \textbf{Dependency Graph}
  \qquad
  \varphi, \psi ~~::=~~
  \emptyset ~~\mid~~
  \gedgeuv ~~\mid~~
  \varphi \sqcup \psi ~~\mid~~
  \Newa\varphi
\]

The term $\emptyset$ represents the empty graph which has no vertices
and no edges.
The unordered pair $\gedgeuv$ represents the graph made of
a single edge connecting the vertices $u$ and $v$.
The term $\varphi\sqcup\psi$ represents the union of
$\varphi$ and $\psi$ whereas $\Newa\varphi$ represents
the same graph as $\varphi$ except that the vertex $a$ is
restricted.
The usual notions of free and bound names apply to dependency
graphs. We write $\mathsf{fn}(\varphi)$ for the free names of $\varphi$.

\begin{table}
  \[
    \begin{array}{@{}c@{}}
      \inferrule{}{
        \gedgeuv \greduv \emptyset
      }
      ~~\defrule{g-axiom}
      \qquad
      \inferrule{
        \varphi \greduv \varphi'
      }{
        \varphi \sqcup \psi \greduv \varphi' \sqcup \psi
      }
      ~~\defrule{g-left}
      \qquad
      \inferrule{
        \psi \greduv \psi'
      }{
        \varphi \sqcup \psi \greduv \varphi \sqcup \psi'
      }
      ~~\defrule{g-right}
      \\\\
      \inferrule{
        \varphi \greduv \psi
        \\
        a\neu,v
      }{
        \Newa\varphi \greduv \Newa\psi
      }
      ~~\defrule{g-new}
      \qquad
      \inferrule{
        \varphi \greduw \psi
        \\
        \psi \gred\NameWv \varphi'
      }{
        \varphi \greduv \varphi'
      }
      ~~\defrule{g-trans}
    \end{array}
  \]
  \caption{\label{tab:dgraph} Labelled transitions of dependency graphs.}
\end{table}

To define the semantics of a dependency graph we use the labelled
transition system of Table~\ref{tab:dgraph}.  A label
$\glabeluv$ represents a path connecting $u$ with
$v$. So, a relation $\varphi \greduv \varphi'$
means that $u$ and $v$ are connected in $\varphi$ and
$\varphi'$ describes the residual edges of $\varphi$ that have not
been used for building the path between $u$ and $v$.  The
paths of $\varphi$ are built from the edges of $\varphi$ (\emph{cf.}\xspace
\refrule{g-axiom}) connected by shared vertices (\emph{cf.}\xspace
\refrule{g-trans}). Restricted names cannot be observed in labels,
but they may contribute in building paths in the graph (\emph{cf.}\xspace
\refrule{g-new}).

\begin{definition}[graph acyclicity and entailment]
  \label{def:grel}
  Let
  $\grel\varphi \stackrel{\text{\tiny def}}= \set{ \pairuv \mid
    \exists\varphi': \varphi \greduv \varphi' }$ be the
  \emph{dependency relation} generated by $\varphi$.
  %
  We say that $\varphi$ is \emph{acyclic} if $\grel\varphi$ is
  irreflexive.
  %
  We say that $\varphi$ \emph{entails} $\psi$, written
  $\varphi \Rightarrow \psi$, if
  $\grel\psi \subseteq \grel\varphi$.
\end{definition}

Note that $\sqcup$ is commutative, associative and has $\emptyset$ as
unit with respect to $\grel\cdot$ (see
Appendix~\ref{sec:prop_graphs}).
These properties of dependency graphs are key to prove that typing
is preserved by structural congruence on processes.
Note also that $\sqcup$ is \emph{not} idempotent. Indeed,
$\gedgeuv \sqcup \gedgeuv$ is cyclic whereas
$\gedgeuv$ is not. The following example motivates the
reason why the multiplicity of dependencies is important.

\begin{example}
  \label{ex:multiplicity}
  Consider the reduction
  \[
    P \stackrel{\text{\tiny def}}=
    \Newa
    \Newb\parens{
      \Senda\TagAb
      \mathbin\ttbar
      \Senda\TagBb
      \mathbin\ttbar
      \Receivea\Tag[A]\Var[x]
      \Receivea\Tag[B]\Var[y]
      \Freea
      \Send\Var[x]\Tag\Var[y]
    }
    \rightarrow^*
    \Newb\Sendb\Tagb
    \arrownot\red
  \]
  and observe that $P$ stores two messages in the mailbox
  $a$, each containing a reference to the mailbox
  $b$. The two variables $\Var[x]$ and $\Var[y]$, which were
  syntactically different in $P$, have been unified into
  $b$ in the reduct, which is deadlocked.
  %
  Unlike previous examples of deadlocked processes, which resulted
  from mutual dependencies between different mailboxes, in this case
  the deadlock is caused by the same dependency
  $\gedgeab$ arising twice.
  %
  \hfill$\blacksquare$
\end{example}

\section{Inferring Mailbox Patterns}
\label{sec:inference}

Pattern expressions
\[
  \mathbb{E}, \mathbb{F} ~~::=~~
  \mathbb{0} ~~\mid~~
  \mathbb{1} ~~\mid~~
  \alpha ~~\mid~~
  \tmessage\Tag{\seqof\Capability\seqof\PatternVar} ~~\mid~~
  \mathbb{E} + \mathbb{F} ~~\mid~~
  \mathbb{E} \cdot \mathbb{F} ~~\mid~~
  \mathbb{E}^{\ast}
\]

Shape of constraints
\[
  \varphi ~~::=~~
  \mkconstant{False} ~~\mid~~
  \mathbb{E} \subp \mathbb{F} ~~\mid~~
  \kappa\mathbb{E} \leqslant \kappa\mathbb{F} ~~\mid~~
  \alpha \ll \tmessage\Tag{\seqof\Capability\seqof\PatternVar}
\]

\begin{table}
  \begin{center}
    \[
      \begin{array}{@{}c@{}}
        \inferrule[\defrule{i-idle}]{
        }{
          \itp\Idle\emptyset\emptyset\emptyset
        }
        \qquad
        \inferrule[\defrule{i-message}]{
        }{
          \itp{\Sendu\Tag\seqof\NameV}{
            u : \ttemark\beta,
            \seqof\NameV : \seqof{\kappa\alpha}
          }{
            \gedgeu{\set\seqof\NameV}
          }{
            \set{
              \ttemark\beta
              \leqslant
              \ttemark\tmessage\Tag{\seqof{\kappa\alpha}}
            }
          }
        }
        \\\\
        \inferrule[\defrule{i-invoke}]{
          \mathstrut
        }{
          \itp{\invoke\RecVar\seqof\NameV}{
            \seqof\NameV : \seqof{\kappa\alpha}
          }{
            \varphi\subst\seqof\NameV\seqof\NameU
          }{
            \set{
              \seqof{\kappa\alpha}
              \leqslant
              \seqof{\kappa\gamma}
            }
          }
        }
        ~~~\RecVar : (\seqof\NameU : \seqof{\kappa\gamma}; \varphi)
        \qquad
        \inferrule[\defrule{i-sub}]{
          \itpP\Gamma\varphi\mathcal{C}
        }{
          \itpP{\Gamma, u : \kappa\alpha}\varphi{
            \mathcal{C} \cup \set{ \kappa\alpha \leqslant \kappa\mathbb{1} }
          }
        }
        \\\\
        \inferrule[\defrule{i-input}]{
          \itp{P_i}{
            u : \ttqmark\beta_i, \Gamma_i, \seqof\VarX_i : \seqof\Capability_i\seqof\PatternVar_i
          }{
            \varphi_i
          }{
            \mathcal{C}_i
          }
          ~{}^{(\range{i}{1}{n})}
          \\
          \Delta_1 = \Gamma_1
          \\
          \MergeContexts{\Delta_{i-1}}{\Gamma_i}{\Delta_i}{\mathcal{C}_i'}
          ~{}^{(\range{i}{2}{n})}
        }{
          \textstyle
          \itp{
            \Branch[\range{i}{1}{n}]\Receiveu{\Tag_i}{\seqof\VarX_i}P_i
          }{
            u : \ttqmark\beta, \Delta_n
          }{
            \gedgeu{\mathsf{dom}(\Delta_n)}
          }{
            \begin{lines}[t]
              \textstyle
              \set{ \ttqmark\beta \leqslant \ttqmark\sum_{\range{i}{1}{n}} \tmessage{\Tag_i}{\seqof\Capability_i\seqof\PatternVar_i} \cdot \beta_i}
              \\
              \textstyle
              {}
              \cup
              \bigcup_{\range{i}{1}{n}}\parens{
                \mathcal{C}_i
                \cup
                \mathcal{C}_i'
                \cup
                \set{
                  \beta_i \ll \tmessage{\Tag_i}{\seqof\Capability_i\seqof\PatternVar_i}
                }
              }
            }
          \end{lines}
        }
        \\\\
        \inferrule[\defrule{i-par}]{
          \itp{P_i}{\Gamma_i}{\varphi_i}{\mathcal{C}_i}
          ~{}^{(i=1,2)}
          \\
          \JoinContexts{\Gamma_1}{\Gamma_2}{\Gamma}{\mathcal{C}}
        }{
          \itp{P_1 \mathbin\ttbar P_2}{\Gamma}{\varphi_1 \sqcup \varphi_2}{
            \mathcal{C} \cup \mathcal{C}_1 \cup \mathcal{C}_2
          }
        }
        ~~~\text{$\varphi_1 \sqcup \varphi_2$ acyclic}
        \qquad
        \inferrule[\defrule{i-new}]{
          \itpP{\Gamma, a : \ttqmark\alpha}{\varphi}{\mathcal{C}}
        }{
          \itp{\NewaP}{\Gamma}{\Newa\varphi}{
            \mathcal{C} \cup \set{\ttqmark\mathbb{1} \leqslant \ttqmark\alpha}
          }
        }
      \end{array}
    \]
  \end{center}
  \caption{
    \label{tab:inference}
    Pattern inference rules.
  }
\end{table}

merge operator
\[
  \inferrule{
  }{
    \MergeContexts\emptyset\EmptyContext\emptyset\emptyset
  }
  \qquad
  \inferrule{
    \MergeContexts{\Gamma_1}{\Gamma_2}{\Delta}\mathcal{C}
  }{
    \MergeContexts{
      u : \kappa\alpha_1, \Gamma_1
    }{
      u : \kappa\alpha_2, \Gamma_2
    }{
      u : \kappa\alpha, \Gamma
    }{
      \mathcal{C} \cup \set[i=1,2]{ \kappa\alpha \leqslant \kappa\alpha_i }
    }
  }
\]

join operator
\[
  \begin{array}{@{}c@{}}
    \inferrule{
    }{
      \JoinContexts\Gamma\emptyset\Gamma\emptyset
    }
    \qquad
    \inferrule{
    }{
      \JoinContexts\emptyset\Gamma\Context\emptyset
    }
    \qquad
    \inferrule{
      \JoinContexts{\Gamma_1}{\Gamma_2}{\Gamma}{\mathcal{C}}
    }{
      \JoinContexts{
        u : \ttemark\alpha_1, \Gamma_1
      }{
        u : \ttemark\alpha_2, \Gamma_2
      }{
        u : \ttemark\alpha, \Gamma
      }{
        \mathcal{C} \cup \set{ \ttemark\alpha \leqslant \ttemark\parens{\alpha_1 \cdot \alpha_2} }
      }
    }
    \\\\
    \inferrule{
      \JoinContexts{\Gamma_1}{\Gamma_2}{\Gamma}{\mathcal{C}}
    }{
      \JoinContexts{
        u : \ttemark\alpha_1, \Gamma_1
      }{
        u : \ttqmark\alpha_2, \Gamma_2
      }{
        u : \ttqmark\alpha, \Gamma
      }{
        \mathcal{C} \cup \set{ \ttqmark\parens{\alpha_1 \cdot \alpha} \leqslant \ttqmark\alpha_2 }
      }
    }
  \end{array}
\]

\section{Introduction}
\label{sec:introduction}

Message passing is a key mechanism used to coordinate concurrent
processes.
The order in which a process consumes messages may coincide with the
order in which they arrive at destination (\emph{ordered
  processing}) or may depend on some intrinsic property of the
messages themselves, such as their priority, their tag, or the shape
of their content (\emph{out-of-order or selective processing}).
Ordered message processing is common in networks of processes
connected by point-to-point \emph{channels}.
Out-of-order message processing is common in networks of processes
using \emph{mailboxes}, into which processes concurrently store
messages and from which one process selectively receives messages.
This communication model is typically found in the various
implementations of actors~\cite{HewittEtAl73,Agha86} such as
Erlang~\cite{Armstrong13}, Scala and Akka
actors~\cite{HallerSommers11}, CAF~\cite{CharoussetHiesgenSchmidt16}
and Kilim~\cite{SrinivasanMycroft08}.
Non-uniform, concurrent
objects~\cite{RavaraVasconcelos00,Puntigam01,CrafaPadovani17} are
also examples of out-of-order message processors. For example, a
busy lock postpones the processing of any $\Tag[acquire]$ message
until it is released by its current owner.
Out-of-order message processing adds further complexity to the
challenging task of concurrent and parallel application development:
storing a message into the wrong mailbox or at the wrong time,
forgetting a message in a mailbox, or relying on the presence of a
particular message that is not guaranteed to be found in a mailbox
are programming mistakes that are easy to do and hard to detect
without adequate support from the language and its development
tools.

\InputScala[label=lst:account,caption=An example of Scala actor taken from the \texttt{Savina} benchmark suite~\cite{ImamSarkar14}.]{Account.scala}

The Scala actor in Listing~\ref{lst:account}, taken from the
\texttt{Savina} benchmark suite~\cite{ImamSarkar14}, allows us to
illustrate some of the subtle pitfalls that programmers must
carefully avoid when dealing with out-of-order message processing.
The \lstinline[language=Scala,style=INLINE]{process} method matches messages found in the actor's
mailbox according to their type.
If a message of type \lstinline[language=Scala,style=INLINE]{DebitMessage} is found, then \lstinline[language=Scala,style=INLINE]{balance}
is incremented by the deposited amount and the actor requesting the
operation is notified with a \lstinline[language=Scala,style=INLINE]{ReplyMessage}
(lines~\ref{begin.account.debit}--\ref{end.account.debit}).
If a message of type \lstinline[language=Scala,style=INLINE]{CreditMessage} is found, \lstinline[language=Scala,style=INLINE]{balance} is
decremented by the amount that is transferred to \lstinline[language=Scala,style=INLINE]{recipient}
(lines~\ref{begin.account.credit}--\ref{account.credit.send}). Since
the operation is meant to be atomic, the actor temporarily changes
its behavior and waits for a \lstinline[language=Scala,style=INLINE]{ReplyMessage} from \lstinline[language=Scala,style=INLINE]{recipient}
signalling that the transfer is complete, before notifying
\lstinline[language=Scala,style=INLINE]{sender} in turn
(lines~\ref{account.credit.wait}--\ref{end.account.credit}).
A message of type \lstinline[language=Scala,style=INLINE]{StopMessage} terminates the actor
(line~\ref{account.stop}).

Note how the correct execution of this code depends on some key
assumptions:
\begin{itemize}
\item \lstinline[language=Scala,style=INLINE]{ReplyMessage} should be stored in the actor's mailbox only
  when the actor is involved in a transaction, or else the message
  would trigger the ``catch all'' clause that throws a ``unsupported
  message'' exception
  (lines~\ref{begin.account.unknown}--\ref{end.account.unknown}).
\item No debit or credit message should be in the actor's mailbox by
  the time it receives \lstinline[language=Scala,style=INLINE]{StopMessage}, or else some critical
  operations affecting the balance would not be performed.
\item Two distinct accounts should not try to simultaneously
  initiate a transaction with each other. If this were allowed, each
  account could consume the credit message found in its own mailbox
  and then deadlock waiting for a reply from the other account
  (lines~\ref{account.credit.wait}--\ref{end.account.credit}).
\end{itemize}

Static analysis techniques that certify the validity of assumptions
like these can be valuable for developers.  For example, session
types~\cite{HuttelEtAl16} have proved to be an effective formalism
for the enforcement of communication protocols and have been applied
to a variety of programming paradigms and
languages~\cite{AnconaEtAl16}, including those based on mailbox
communications~\cite{MostrousVasconcelos11,CharalambidesDingesAgha16,Fowler16,NeykovaYoshida16}.
However, session types are specifically designed to address
point-to-point, ordered interactions over
channels~\cite{Honda93}. Retrofitting them to a substantially
different communication model calls for some inevitable compromises
on the network topologies that can be addressed and forces
programmers to give up some of the flexibility offered by unordered
message processing.

Another aspect that complicates the analysis of actor systems is
that the pure actor model as it has been originally
conceived~\cite{HewittEtAl73,Agha86} does not accurately reflect the
actual practice of actor programming. In the pure actor model, each
actor owns a single mailbox and the only synchronization mechanism
is message reception from such mailbox.
However, it is a known fact that the implementation of complex
coordination protocols in the pure actor model is
challenging~\cite{VarelaAgha01,TasharofiDingesJohnson13,ImamSarkar14bis,ChatterjeeEtAl16}. These
difficulties have led programmers to mix the actor model with
different concurrency
abstractions~\cite{ImamSarkar12,TasharofiDingesJohnson13}, to extend
actors with controlled forms of synchronization~\cite{VarelaAgha01}
and to consider actors with multiple/first-class
mailboxes~\cite{Haller12,ImamSarkar14bis,ChatterjeeEtAl16}.
In fact, popular implementations of the actor model feature
disguised instances of multiple/first-class mailbox usage, even if
they are not explicitly presented as such: in Akka, the messages
that an actor is unable to process immediately can be temporarily
stashed into a different mailbox~\cite{Haller12}; in Erlang, hot
code swapping implies transferring at runtime the input capability
on a mailbox from a piece of code to a different
one~\cite{Armstrong13}.

In summary, there is still a considerable gap between the scope of
available approaches used to analyze mailbox-based communicating
systems and the array of features used in programming these
systems. To help narrowing this gap, we make the following
contributions:
\begin{itemize}
\item We introduce \emph{mailbox types}, a new kind of behavioral
  types with a simple and intuitive semantics embodying the
  unordered nature of mailboxes. Mailbox types allow us to describe
  mailboxes subject to selective message processing as well as
  mailboxes concurrently accessed by several
  processes. Incidentally, mailbox types also provide precise
  information on the size and reachability of mailboxes that may
  lead to valuable code optimizations.
\item We develop a mailbox type system for the \emph{mailbox
    calculus}, a mild extension of the asynchronous
  $\pi$-calculus~\cite{SangiorgiWalker01} featuring tagged messages,
  selective inputs and first-class mailboxes.  The mailbox calculus
  allows us to address a broad range of systems with dynamic
  topology and varying number of processes possibly using a mixture
  of concurrency models (including multi-mailbox actors) and
  abstractions (such as locks and futures).
\item We prove three main properties of well-typed processes: the
  absence of failures due to unexpected messages (\emph{mailbox
    conformance}); the absence of pending activities and messages in
  irreducible processes (\emph{deadlock freedom}); for a non-trivial
  class of processes, the guarantee that every message can be
  eventually consumed (\emph{junk freedom}).
\item We illustrate the expressiveness of mailbox types by
  presenting well-typed encodings of known concurrent objects (locks
  and futures) and actor benchmarks (atomic transactions and
  master-workers parallelism) and of binary sessions extended with
  forks and joins. In discussing these examples, we emphasize the
  impact of out-of-order message processing and of first-class
  mailboxes.
\end{itemize}

\subparagraph*{Structure of the paper.}
We start from the definition of the \emph{mailbox calculus} and of
the properties we expect from well-typed processes
(Section~\ref{sec:model}).
We introduce mailbox types (Section~\ref{sec:types}) and dependency
graphs (Section~\ref{sec:graphs}) for tracking mailbox dependencies
in processes that use more than one. Then, we present the typing
rules (Section~\ref{sec:rules}) and the soundness results of the
type system (Section~\ref{sec:properties}).
In the latter part of the paper, we discuss a few more complex
examples (Section~\ref{sec:examples}), related work
(Section~\ref{sec:related}) and ideas for further developments
(Section~\ref{sec:conclusions}).
Additional definitions and proofs can be found in
Appendices~\ref{sec:extra_properties}--\ref{sec:example_readers_writer}.

\section{The Mailbox Calculus}
\label{sec:model}

\begin{table}
  \begin{center}
    \[
      \begin{array}[t]{@{}rr@{~}c@{~}ll@{}}
        \textbf{Process} & P, Q
        & ::= & \mkkeyword{done} & \text{(termination)}
        \\
        & & | & \invoke\RecVar\seqof\NameU & \text{(invocation)}
        \\
        & & | & G & \text{(guarded process)}
        \\
        & & | & \Sendu\Tag\seqof\NameV & \text{(stored message)}
        \\
        & & | & P \mathbin\ttbar Q & \text{(parallel composition)}
        \\
        & & | & \NewaP & \text{(mailbox restriction)}
        \\\\
        \textbf{Guard} & G, H
        & ::= & \Failu & \text{(runtime error)}
        \\
        & & | & \FreeuP & \text{(mailbox deletion)}
        \\
        & & | & \Receiveu\Tag\seqof\VarXP & \text{(selective receive)}
        \\
        & & | & G + H & \text{(guard composition)}
      \end{array}
    \]
  \end{center}
  \caption{\label{tab:processes} Syntax of the mailbox calculus.}
\end{table}

We assume given an infinite set of \emph{variables} $\Var[x]$,
$\Var[y]$, an infinite set of \emph{mailbox names} $a$,
$b$, a set of \emph{tags} $\Tag$ and a finite set of
\emph{process variables} $\RecVar$.
We let $u$, $v$ range over variables and mailbox names
without distinction.
Throughout the paper we write $\seqof{e}$ for possibly empty
sequences $e_1, \dots, e_n$ of various entities. For example,
$\seqof\NameU$ stands for a sequence $u_1,\dots,u_n$ of names and
$\set\seqof\NameU$ for the corresponding set.

The syntax of the \emph{mailbox calculus} is shown in
Table~\ref{tab:processes}.
The term $\mkkeyword{done}$ represents the terminated process that performs no
action.
The term $\Sendu\Tag\seqof\NameV$ represents a message stored in
mailbox $u$. The message has tag $\Tag$ and arguments $\seqof\NameV$.
The term $P \mathbin\ttbar Q$ represents the parallel
composition of $P$ and $Q$ and
$\NewaP$ represents a restricted mailbox $a$
with scope $P$.
The term $\invoke\RecVar\seqof\NameU$ represents the invocation of the
process named $\RecVar$ with parameters $\seqof\NameU$. For each process
variable $\RecVar$ we assume that there is a corresponding
\emph{global process definition} of the form
$\define\RecVar\seqof\VarXP$.
A guarded process $G$ is a composition of actions.
The action $\Failu$ represents the process that fails with an
error for having received an unexpected message from mailbox
$u$.
The action $\FreeuP$ represents the process that deletes
the mailbox $u$ if it is empty and then continues as $P$.
The action $\Receiveu\Tag\seqof\VarXP$ represents the process
that receives an $\Tag$-tagged message from mailbox $u$ then
continues as $P$ with $\seqof\VarX$ replaced by the message's
arguments.
A compound guard $G + H$ offers all the actions
offered by $G$ and $H$. We assume that all actions in
the same guard refer to the same mailbox $u$.
The notions of free and bound names of a process $P$ are
standard and respectively denoted by $\mathsf{fn}(P)$ and
$\mathsf{bn}(P)$.

The operational semantics of the mailbox calculus is mostly
conventional. We use the structural congruence relation $\equiv$
defined below to rearrange equivalent processes:
\[
  \begin{array}{@{}*{3}{r@{~}c@{~}l}@{}}
    \Faila + G & \equiv & G
    &
    G + H & \equiv & H + G
    &
    G + (H + H') & \equiv & (G + H) + H'
    \\
    \mkkeyword{done} \mathbin\ttbar P & \equiv & P
    &
    P \mathbin\ttbar Q & \equiv & Q \mathbin\ttbar P
    &
    P \mathbin\ttbar (Q \mathbin\ttbar R)
    & \equiv &
    (P \mathbin\ttbar Q) \mathbin\ttbar R
    \\
    & & &
    \Newa\NewbP
    & \equiv &
    \Newb\NewaP
    &
    \NewaP \mathbin\ttbar Q
    & \equiv &
    \Newa(P \mathbin\ttbar Q)
    \quad\text{if $a \not\in \mathsf{fn}(Q)$}
  \end{array}
\]

Structural congruence captures the usual commutativity and
associativity laws of action and process compositions, with
$\Fail{}$ and $\mkkeyword{done}$ acting as the respective units.  Additionally,
the order of mailbox restrictions is irrelevant and the scope of a
mailbox may shrink or extend dynamically.
The reduction relation $\rightarrow$ is inductively defined by the rules
\[
  \begin{array}{rr@{~}c@{~}ll}
    \defrule{r-read} &
    \Senda\Tag{\seqofc}
    \mathbin\ttbar
    \Receivea\Tag\seqof\VarXP + G
    & \rightarrow &
    P\subst{\seqofc}\seqof\VarX
    \\
    \defrule{r-free} &
    \Newa\parens{\FreeaP + G}
    & \rightarrow &
    P
    \\
    \defrule{r-def} &
    \invoke\RecVar{\seqofc}
    & \rightarrow &
    P\subst{\seqofc}\seqof\VarX
    & \text{if $\define\RecVar\seqof\VarXP$}
    \\
    \defrule{r-par} &
    P \mathbin\ttbar R
    & \rightarrow &
    Q \mathbin\ttbar R
    & \text{if $P \rightarrow Q$}
    \\
    \defrule{r-new} &
    \NewaP
    & \rightarrow &
    \NewaQ
    & \text{if $P \rightarrow Q$}
    \\
    \defrule{r-struct} &
    P
    & \rightarrow &
    Q
    & \text{if $P \equiv P' \rightarrow Q' \equiv Q$}
  \end{array}
\]
where $P\subst\seqof\MailboxC\seqof\VarX$ denotes the usual
capture-avoiding replacement of the variables $\seqof\VarX$ with the
mailbox names $\seqof\MailboxC$.
Rule~\refrule{r-read} models the selective reception of an
$\Tag$-tagged message from mailbox $a$, which erases all the
other actions of the guard.
Rule~\refrule{r-free} is triggered when the process is ready to
delete the empty mailbox $a$ and no more messages can be
stored in $a$ because there are no other processes in the
scope of $a$.
Rule~\refrule{r-def} models a process invocation by replacing the
process variable $\RecVar$ with the corresponding definition.
Finally, rules~\refrule{r-par}, \refrule{r-new} and
\refrule{r-struct} close reductions under parallel compositions,
name restrictions and structural congruence.
We write $\rightarrow^*$ for the reflexive and transitive closure of
$\rightarrow$, we write $P \arrownot\red^* Q$ if not
$P \rightarrow^* Q$ and $P \arrownot\red$ if
$P \arrownot\red Q$ for all $Q$.

Hereafter, we will occasionally use numbers and conditionals in
processes. These and other features can be either encoded or added
to the calculus without difficulties.

\begin{example}[lock]
  \label{ex:lock}
  In this example we model a lock as a process that waits for
  messages from a $\Var[self]$ mailbox in which acquisition and
  release requests are stored. The lock is either free or busy. When
  in state free, the lock nondeterministically consumes an
  $\Tag[acquire]$ message from $\Var[self]$. This message indicates the
  willingness to acquire the lock by another process and carries a
  reference to a mailbox into which the lock stores a $\Tag[reply]$
  notification. When in state busy, the lock waits for a
  $\Tag[release]$ message indicating that it is being released:
  \[
    \begin{array}{@{}r@{~}c@{~}l@{}}
      \RecVar[FreeLock](\Var[self]) & \triangleq &
      \Free\Var[self]\mkkeyword{done}
      \\ & + &
      \Receive\Var[self]\Tag[acquire]\Var[owner]
      \invoke\RecVar[BusyLock]{\Var[self],\Var[owner]}
      \\ & + &
      \Receive\Var[self]\Tag[release]{}
      \Fail\Var[self]
      \\
      \RecVar[BusyLock](\Var[self],\Var[owner]) & \triangleq &
      \Send\Var[owner]\Tag[reply]\Var[self] \mathbin\ttbar
      \Receive\Var[self]\Tag[release]{}\invoke\RecVar[FreeLock]\Var[self]
    \end{array}
  \]

  Note the presence of the $\Free[]\Var[self]$ guard in the definition
  of $\RecVar[FreeLock]$ and the lack thereof in $\RecVar[BusyLock]$. In the
  former case, the lock manifests the possibility that no process is
  willing to acquire the lock, in which case it deletes the mailbox
  and terminates. In the latter case, the lock manifests its
  expectation to be eventually released by its current owner.
  %
  Also note that $\RecVar[FreeLock]$ fails if it receives a $\Tag[release]$
  message. In this way, the lock manifests the fact that it can be
  released only if it is currently owned by a process.
  %
  A system where two users $\Var[alice]$ and $\Var[carol]$ compete for
  acquiring $\Var[lock]$ can be modeled as the process
  \begin{equation}
    \label{eq:alice_carol}
    \New\Var[lock]
    \New\Var[alice]
    \New\Var[carol]\parens{
      \invoke\RecVar[FreeLock]\Var[lock]
      \mathbin\ttbar
      \invoke\RecVar[User]{\Var[alice], \Var[lock]}
      \mathbin\ttbar
      \invoke\RecVar[User]{\Var[carol], \Var[lock]}
    }
  \end{equation}
  where
  \[
    \RecVar[User](\Var[self], \Var[lock]) \triangleq
    \Send\Var[lock]\Tag[acquire]\Var[self] \mathbin\ttbar
    \Receive\Var[self]\Tag[reply]{l}
    \parens{
      \Send{l}\Tag[release]{}
      \mathbin\ttbar
      \Free\Var[self]\mkkeyword{done}
    }
  \]

  Note that $\RecVar[User]$ uses the reference $l$ -- as opposed to
  $\Var[lock]$ -- to release the acquired lock. As we will see in
  Section~\ref{sec:rules}, this is due to the fact that it is this
  particular reference to the lock's mailbox -- and not $\Var[lock]$
  itself -- that carries the capability to release the lock.
  %
  \hfill$\blacksquare$
\end{example}

\begin{example}[future variable]
  \label{ex:future}
  A future variable is a one-place buffer that stores the result of
  an asynchronous computation. The content of the future variable is
  set once and for all by the producer once the computation
  completes. This phase is sometimes called \emph{resolution} of the
  future variable. After the future variable has been resolved, its
  content can be retrieved any number of times by the consumers. If
  a consumer attempts to retrieve the content of the future variable
  beforehand, the consumer suspends until the variable is resolved.
  %
  We can model a future variable thus:
  \[
    \begin{array}{@{}r@{~}c@{~}l@{}}
      \RecVar[Future](\Var[self]) & \triangleq & \Receive\Var[self]\Tag[resolve]\Var\invoke\RecVar[Present]{\Var[self],\Var}
      \\
      \RecVar[Present](\Var[self], \Var) & \triangleq &
      \Free\Var[self]\mkkeyword{done}
      \\ & + &
      \Receive\Var[self]\Tag[get]\Var[sender](\Send\Var[sender]\Tag[reply]\Var \mathbin\ttbar \invoke\RecVar[Present]{\Var[self],\Var})
      \\ & + &
      \Receive\Var[self]\Tag[resolve]{}
      \Fail\Var[self]
    \end{array}
  \]

  The process $\RecVar[Future]$ represents an unresolved future variable,
  which waits for a $\Tag[resolve]$ message from the producer. Once
  the variable has been resolved, it behaves as specified by
  $\RecVar[Present]$, namely it satisfies an arbitrary number of
  $\Tag[get]$ messages from consumers but it no longer accepts
  $\Tag[resolve]$ messages.
  %
  \hfill$\blacksquare$
\end{example}

\begin{example}[bank account]
  \label{ex:account}
  Below we see the process definition corresponding to the actor
  shown in Listing~\ref{lst:account}. The structure of the term
  follows closely that of the Scala code:
  \[
    \begin{array}{@{}rcl@{}}
      \RecVar[Account](\Var[self], \Var[balance]) & \triangleq &
      \Receive\Var[self]\Tag[debit]{\Var[amount],\Var[sender]}
      \\ & &
      \Send\Var[sender]\Tag[reply]{}
      \mathbin\ttbar
      \invoke\RecVar[Account]{\Var[self], \Var[balance] + \Var[amount]}
      \\
      & + &
      \Receive\Var[self]\Tag[credit]{\Var[amount],\Var[recipient],\Var[sender]}
      \\ & &
      \Send\Var[recipient]\Tag[debit]{\Var[amount],\Var[self]} \mathbin\ttbar {}
      \\ & &
      \Receive\Var[self]\Tag[reply]{}
      \parens{
        \Send\Var[sender]\Tag[reply]{}
        \mathbin\ttbar
        \invoke\RecVar[Account]{\Var[self], \Var[balance] + \Var[amount]}
      }
      \\
      & + &
      \Receive\Var[self]\Tag[stop]{}
      \Free\Var[self]\mkkeyword{done}
      \\
      & + &
      \Receive\Var[self]\Tag[reply]{}
      \Fail\Var[self]
    \end{array}
  \]

  The last term of the guarded process, which results in a failure,
  corresponds to the catch-all clause in Listing~\ref{lst:account}
  and models the fact that a $\Tag[reply]$ message is not expected to
  be found in the account's mailbox unless the account is involved
  in a transaction. The $\Tag[reply]$ message is received and handled
  appropriately in the $\Tag[credit]$-guarded term.

  We can model a deadlock in the case two distinct bank accounts
  attempt to initiate a transaction with one another. Indeed, we
  have
  \[
    \begin{lines}
      \invoke\RecVar[Account]{\Var[alice], 10} \mathbin\ttbar
      \Send\Var[alice]\Tag[credit]{2, \Var[carol], \Var[bank]} \mathbin\ttbar {}
      \\
      \invoke\RecVar[Account]{\Var[carol], 15} \mathbin\ttbar
      \Send\Var[carol]\Tag[credit]{5, \Var[alice], \Var[bank]}
    \end{lines}
    \rightarrow^*
    \begin{lines}
      \Send\Var[carol]\Tag[debit]{2,\Var[alice]}
      \mathbin\ttbar
      \Receive[]\Var[alice]\Tag[reply]{}\dots \mathbin\ttbar {}
      \\
      \Send\Var[alice]\Tag[debit]{5,\Var[carol]}
      \mathbin\ttbar
      \Receive[]\Var[carol]\Tag[reply]{}\dots
    \end{lines}
  \]
  where both $\Var[alice]$ and $\Var[carol]$ ignore the incoming
  $\Tag[debit]$ messages, whence the deadlock.
  %
  \hfill$\blacksquare$
\end{example}

We now provide operational characterizations of the properties
enforced by our typing discipline. We begin with mailbox
conformance, namely the property that a process never fails because
of unexpected messages.  To this aim, we define a process context
$\mathcal{C}$ as a process in which there is a single occurrence
of an \emph{unguarded hole} $[~]$:
\[
  \mathcal{C}
  ~~::=~~
  [~] ~~\mid~~
  \mathcal{C} \mathbin\ttbar P ~~\mid~~
  P \mathbin\ttbar \mathcal{C} ~~\mid~~
  \Newa\mathcal{C}
\]

The hole is ``unguarded'' in the sense that it does not occur
prefixed by an action. As usual, we write
$\mathcal{C}[P]$ for the process obtained by replacing
the hole in $\mathcal{C}$ with $P$. Names may be captured
by this replacement. A mailbox conformant process never reduces to a
state in which the only action of a guard is $\Fail{}$:

\begin{definition}
  \label{def:mailbox_conformance}
  We say that $P$ is \emph{mailbox conformant} if
  $P \arrownot\red^* \mathcal{C}[\Faila]$ for all
  $\mathcal{C}$ and $a$.
\end{definition}

Looking at the placement of the $\Failu$ actions in earlier
examples we can give the following interpretations of mailbox
conformance: a lock is never released unless it has been acquired
beforehand (Example~\ref{ex:lock}); a future variable is never
resolved twice (Example~\ref{ex:future}); an account will not be
notified of a completed transaction (with a $\Tag[reply]$ message)
unless it is involved in an ongoing transaction
(Example~\ref{ex:account}).

We express deadlock freedom as the property that all irreducible
residuals of a process are (structurally equivalent to) the
terminated process:

\begin{definition}
  \label{def:deadlock_freedom}
  We say that $P$ is \emph{deadlock free} if
  $P \rightarrow^* Q \arrownot\red$ implies
  $Q \equiv \mkkeyword{done}$.
\end{definition}

According to Definition~\ref{def:deadlock_freedom}, if a
deadlock-free process halts we have that: (1) there is no
sub-process waiting for a message that is never produced; (2) every
mailbox is empty. Clearly, this is not the case for the transaction
between $\Var[alice]$ and $\Var[carol]$ in Example~\ref{ex:account}.

\begin{example}[deadlock]
  \label{ex:deadlock}
  Below is another example of deadlocking process using $\RecVar[Future]$
  from Example~\ref{ex:future}, obtained by resolving a future
  variable with the value it does not contain yet:
  \begin{equation}
    \label{eq:future_deadlock}
    \New\Var[f]
    \Newc\parens{
      \invoke\RecVar[Future]\Var[f]
      \mathbin\ttbar
      \Send\Var[f]\TagGetc
      \mathbin\ttbar
      \Receivec\Tag[reply]\Var
      \Freec
      \Send\Var[f]\Tag[put]\Var
    }
  \end{equation}

  Notice that attempting to retrieve the content of a future
  variable not knowing whether it has been resolved is
  legal. Indeed, $\RecVar[Future]$ does not fail if a $\Tag[get]$ message
  is present in the future variable's mailbox before it is
  resolved. Thus, the deadlocked process above is mailbox conformant
  but also an instance of undesirable process that will be ruled out
  by our static analysis technique (\emph{cf.}\xspace
  Example~\ref{ex:future_deadlock}). We will need dependency graphs
  in addition to types to flag this process as ill typed.
  %
  \hfill$\blacksquare$
\end{example}

A property stronger than deadlock freedom is fair termination.  A
fairly terminating process is a process whose residuals always have
the possibility to terminate. Formally:

\begin{definition}
  \label{def:terminating}
  We say that $P$ is \emph{fairly terminating} if
  $P \rightarrow^* Q$ implies $Q \rightarrow^* \mkkeyword{done}$.
\end{definition}

An interesting consequence of fair termination is that it implies
\emph{junk freedom} (also known as lock
freedom~\cite{Kobayashi02,Padovani14B}) namely the property that
every message can be eventually consumed. Our type system does not
guarantee fair termination nor junk freedom in general, but it does
so for a non-trivial sub-class of well-typed processes that we
characterize later on.

\subsection{Proof of mailbox conformance}
\label{sec:proof_conformance}

\begin{lemma}
  \label{lem:fail}
  If $\wtp\Gamma{\mathcal{C}[\Failu]}\varphi$, then
  $\Gamma$ is unreliable.
\end{lemma}
\begin{proof}
  We reason by induction on the derivation of
  $\wtp\Gamma{\mathcal{C}[\Failu]}\varphi$ and by cases on
  the last rule applied, omitting symmetric cases and those ruled
  out by the syntax of $\mathcal{C}$.

  \proofrule{t-guard}
  %
  From \refrule{t-fail} we deduce that
  $\Gamma = u : \ttqmark\mathbb{0}, \Delta$ and we conclude that
  $\Gamma$ is unreliable.

  \proofrule{t-par}
  %
  Suppose, without loss of generality, that
  $\mathcal{C} = P \mathbin\ttbar \mathcal{C}'$.
  %
  Then there exist $\Gamma_1$, $\Gamma_2$, $\varphi_1$ and
  $\varphi_2$ such that $\Gamma = \Gamma_1 \mathbin{\|} \Gamma_2$ and
  $\varphi \Rightarrow \varphi_1 \sqcup \varphi_2$ and
  $\wtp{\Gamma_1}{P}{\varphi_1}$ and
  $\wtp{\Gamma_2}{\mathcal{C}'[\Failu]}{\varphi_2}$.
  %
  From the induction hypothesis we deduce that $\Gamma_2$ is
  unreliable.
  %
  We know that $\Gamma_1$ is usable since all types are assumed to
  be usable, hence we conclude that $\Gamma_1 \mathbin{\|} \Gamma_2$ is
  unreliable by Proposition~\ref{prop:env_mul_reliable}.

  \proofrule{t-new}
  %
  Then $\mathcal{C} = \Newa\mathcal{C}'$ and
  $\wtp{\Gamma, a :
    \ttqmark\mathbb{1}}{\mathcal{C}'[\Failu]}\psi$.
  %
  By induction hypothesis we deduce that
  $\Gamma, a : \ttqmark\mathbb{1}$ is unreliable.
  %
  Since $\ttqmark\mathbb{1}$ is reliable, we conclude that $\Gamma$ is
  unreliable.

  \proofrule{t-sub}
  %
  Then $\wtp\Delta{\mathcal{C}[\Failu]}\psi$ where
  $\Gamma \leqslant \Delta$.
  %
  By induction hypothesis we deduce that $\Delta$ is unreliable
  and we conclude by Proposition~\ref{prop:env_subt_reliable}.
\end{proof}

\begin{lemma}
  \label{lem:conformance}
  If $\wtp\EmptyContextP\varphi$, then
  $P \arrownot\red^* \mathcal{C}[\Faila]$ for all
  $\mathcal{C}$ and $a$.
\end{lemma}
\begin{proof}
  Immediate consequence of Theorem~\ref{thm:sr} and
  Lemma~\ref{lem:fail}.
\end{proof}

\subsection{Proof of deadlock freedom}
\label{sec:proof_deadlock_freedom}

\begin{notation}
  We abbreviate $\wtp\ContextP\varphi$ with
  $\wtp\ContextP{}$ when the dependency graph $\varphi$ is
  irrelevant.
\end{notation}

\begin{notation}
  Let $\wtp\ContextP{}$ and $u\in\mathsf{fn}(P)$. We write
  $u^\tau \in P$ if $u\in\mathsf{fn}(P)$ and there is
  a judgment of the form $\wtp{\Delta, u : \tau}Q{}$
  in the derivation tree of $\wtp\ContextP{}$. Similarly for
  guards.
\end{notation}

\begin{definition}
  We say that $Q$ occurs \emph{unguarded} in $P$ if
  $P = \mathcal{C}[Q]$ for some
  $\mathcal{C}$.
\end{definition}

\begin{lemma}[output occurrence]
  \label{lem:output_occurrence}
  If $\wtp{a : \ttemarkE, \Gamma}P{}$ and
  $\Gamma$ is reliable, then there exist $n\geq 0$ and
  $F_1, \dots, F_n$ such that
  $F_1 \cdots F_n \subp E$ and
  $a^{\ttemarkF_i} \in P$ for all
  $1 \leq i\leq n$. Furthermore, the $a^{\ttemarkF_i}$
  occurrences account for all of the unguarded messages stored into
  $a$ by $P$.
\end{lemma}
\begin{proof}
  By induction on the typing derivation and by cases on the last
  typing rule applied. The fact that all of the unguarded messages
  stored into $a$ by $P$ are considered follows from
  the structure of the proof, which visits every sub-process of
  $P$ in which $a$ may occur free.

  \proofrule{t-done}
  %
  This case is impossible because $\mkkeyword{done}$ is well typed in the empty
  context only.

  \proofrule{t-msg}
  %
  Then $P = \Sendu\Tag\seqof\NameV$ and
  $a : \ttemarkE, \Gamma = u :
  \ttemark\tmessage\Tag\seqof\TypeT, \seqof\NameV : \seqof\TypeT$ where $a$ is
  either $u$ or one of the $v_i$.
  %
  We conclude by taking $n \stackrel{\text{\tiny def}}= 1$ and
  $F_1 \stackrel{\text{\tiny def}}= E$.

  \proofrule{t-def}
  %
  Similar to the previous case.

  \proofrule{t-par}
  %
  Then $P = P_1 \mathbin\ttbar P_2$ and
  $a : \ttemarkE, \Gamma = \Gamma_1 \mathbin{\|} \Gamma_2$
  and $\wtp{\Gamma_i}{P_i}{}$ for every $i=1,2$.
  %
  From the hypothesis that $\Gamma$ is reliable, the assumption
  that all types are usable and
  Proposition~\ref{prop:env_mul_reliable} we deduce that
  $\Gamma_1$ and $\Gamma_2$ are reliable.
  %
  We discuss two interesting sub-cases:
  \begin{itemize}
  \item Suppose $\Gamma_1 = a : \ttemarkE, \Gamma_1'$
    and $a \not\in\mathsf{dom}(\Gamma_2)$.
    %
    Then $a \not\in \mathsf{fn}(P_2)$ and we conclude from the
    induction hypothesis on $P_1$.
  \item Suppose $\Gamma_1 = a : \ttemarkE_1, \Gamma_1'$
    and $\Gamma_2 = a : \ttemarkE_2, \Gamma_2'$ and
    $E = E_1 \cdot E_2$.
    %
    From the induction hypothesis we deduce that there exist
    $n_1 \geq 0$ and $n_2 \geq 0$ and
    $F_1', \dots, F_{n_1}'$ and
    $F_1'', \dots, F_{n_2}''$ such that
    $F_1' \cdots F_{n_1}' \subp E_1$ and
    $F_1'' \cdots F_{n_2}'' \subp E_2$ and
    $a^{\ttemarkF_i'} \in P_1$ for all
    $1\leq i\leq n_1$ and
    $a^{\ttemarkF_i''} \in P_2$ for all
    $1\leq i\leq n_2$.
    %
    We conclude by taking $n \stackrel{\text{\tiny def}}= n_1 + n_2$ and
    $F_1, \dots, F_n \stackrel{\text{\tiny def}}= F_1', \dots,
    F_{n_1}', F_1'', \dots, F_{n_2}''$.
  \end{itemize}

  \proofrule{t-new}
  %
  Then $P = \NewcQ$ and
  $\wtp{a : \ttemarkE, \Gamma, c :
    \ttqmark\mathbb{1}}Q{}$.
  %
  Since $\ttqmark\mathbb{1}$ is reliable we conclude by the induction
  hypothesis.

  \proofrule{t-guard}
  %
  Then $P = G$ and $\wtg\ContextG$.
  %
  We conclude by the induction hypothesis.

  \proofrule{t-sub}
  %
  Then $\wtp\ContextBP{}$ where
  $a : \ttemarkE, \Gamma \leqslant \Delta$.
  %
  We have two possibilities:
  \begin{itemize}
  \item Suppose $a\in\mathsf{dom}(\Delta)$.
    %
    Then $\Delta = a : \ttemarkE', \Delta'$ where
    $E' \subp E$ and $\Gamma \leqslant \Delta'$.
    %
    From Proposition~\ref{prop:env_subt_reliable} we deduce that
    $\Delta'$ is reliable.
    %
    We conclude by the induction hypothesis using transitivity of
    $\subp$.
  \item Suppose $a\not\in\mathsf{dom}(\Delta)$.
    %
    Then $a\not\in\mathsf{fn}(P)$ and $\ttemarkE$ is
    irrelevant, meaning that $\mathbb{1} \subp E$.
    %
    We conclude by taking $n \stackrel{\text{\tiny def}}= 0$.
  \end{itemize}

  \proofrule{t-fail}
  %
  This case is impossible because $\Gamma$ is reliable by
  hypothesis.

  \proofrule{t-free}
  %
  Then $P = \FreeuQ$ and
  $a : \ttemarkE, \Gamma = u : \ttqmark\mathbb{1}, \Delta$
  and $\wtp\ContextBQ{}$.
  %
  Clearly $a \ne u$. Also, from the hypothesis that
  $\Gamma$ is reliable we deduce that $\Delta$ is reliable.
  %
  We conclude by the induction hypothesis.

  \proofrule{t-in}
  %
  Then $P = \Receiveu\Tag\seqof\VarXQ$ and
  $a : \ttemarkE, \Gamma = u :
  \ttqmark(\tmessage\Tag\seqof\TypeT \cdot F), \Delta$ and
  $\wtp{u : \ttqmarkF, \Delta, \seqof\VarX :
    \seqof\TypeT}Q{}$.
  %
  Clearly $a \ne u$ therefore
  $\Delta = a : \ttemarkE, \Delta'$.
  %
  From the hypothesis that $\Gamma$ is reliable we deduce that
  $F \not\subp \mathbb{0}$.
  %
  From the assumption that argument types are reliable we deduce
  that $u : \ttqmarkF, \Delta, \seqof\VarX : \seqof\TypeT$ is
  reliable.
  %
  We conclude by the induction hypothesis.

  \proofrule{t-branch}
  %
  Then $P = G_1 + G_2$ and
  $a : \ttemarkE, \Gamma = u : \ttqmark(E_1
  + E_2), \Delta$ and
  $\wtg{u : \ttqmarkE_i, \Delta}{G_i}$ for every
  $i=1,2$.
  %
  Clearly $a \ne u$, therefore
  $\Delta = a : \ttemarkE, \Delta'$.
  %
  From the hypothesis that $\Gamma$ is reliable we deduce that
  $E_1 + E_2 \not\subp \mathbb{0}$.  Suppose,
  without loss of generality, that $E_1 \not\subp \mathbb{0}$.
  %
  We conclude by the induction hypothesis on $G_1$.
\end{proof}

\begin{lemma}[input occurrence]
  \label{lem:input_occurrence}
  If $\wtp{a : \ttqmarkE, \Gamma}P{}$ and
  $\Gamma$ is reliable and
  $\mathtt{M} \cdot F \subp E$ and
  $F \not\subp \mathbb{0}$, then there exist $\mathtt{M}'$ and
  $F'$ such that $\mathtt{M} \subp \mathtt{M}'$ and
  $F' \not\subp \mathbb{0}$ and
  $a^{\ttqmark\mathtt{M}'\tmulF'} \in P$.
\end{lemma}
\begin{proof}
  By induction on the derivation of
  $\wtp{a : \ttqmarkE, \Gamma}P{}$ and by cases
  on the last rule applied, recalling that a guard is also a
  process.

  \proofrule{t-done}
  %
  This case is impossible because $\mkkeyword{done}$ is well typed in the empty
  context only.

  \proofrule{t-msg}
  %
  Then $P = \Sendu\Tag\seqof\NameV$ and
  $a : \ttqmarkE, \Gamma = u :
  \ttemark\tmessage\Tag\seqof\TypeT, \seqof\NameV : \seqof\TypeT$.
  %
  Clearly $a \ne u$, so we conclude by taking
  $\mathtt{M} \stackrel{\text{\tiny def}}= \mathtt{M}'$ and
  $F' \stackrel{\text{\tiny def}}= F$.

  \proofrule{t-def}
  %
  Similar to the previous case.

  \proofrule{t-par}
  %
  Then $P = P_1 \mathbin\ttbar P_2$ and
  $a : \ttqmarkE, \Gamma = \Gamma_1 \mathbin{\|} \Gamma_2$
  and $\wtp{\Gamma_i}{P_i}{}$ for $i=1,2$.
  %
  We only discuss one interesting case when
  $\Gamma_1 = a : \ttemarkE_1, \Gamma_1'$ and
  $\Gamma_2 = a : \ttqmark(E_1 \cdot E),
  \Gamma_2'$.
  %
  From the assumption that all types are usable we know that
  $E_1 \not\subp \mathbb{0}$ and both $\Gamma_1'$ and
  $\Gamma_2'$ are usable.
  %
  From the hypothesis that $\Gamma$ is reliable we deduce that
  $\Gamma_1' \mathbin{\|} \Gamma_2'$ is also reliable.
  %
  From Proposition~\ref{prop:env_mul_reliable} we deduce that
  $\Gamma_1'$ and $\Gamma_2'$ are both reliable.
  %
  From the hypothesis $\mathtt{M} \cdot F \subp E$
  and the precongruence of $\subp$ we deduce
  $\mathtt{M} \cdot E_1 \cdot F \subp E_1
  \cdot E$.
  %
  From $E_1 \not\subp \mathbb{0}$ and the hypothesis
  $F \not\subp \mathbb{0}$ we deduce
  $E_1 \cdot F \not\subp \mathbb{0}$.
  %
  We conclude by the induction hypothesis.

 \proofrule{t-new}
  %
  Then $P = \NewcQ$ and
  $\wtp{a : \ttqmarkE, \Gamma, c :
    \ttqmark\mathbb{1}}Q{}$.
  %
  Observe that $\ttqmark\mathbb{1}$ is reliable, so we can conclude by the
  induction hypothesis.

  \proofrule{t-sub}
  %
  Then $\wtp\ContextBP$ for some $\Delta$ such that
  $a : \ttqmarkE, \Gamma \leqslant \Delta$, which
  implies $\Delta = \ttqmarkE', \Delta'$ where
  $E \subp E'$ and $\Gamma \leqslant \Delta'$.
  %
  We have
  $\mathtt{M} \cdot F \subp E \subp E'$ by
  transitivity of $\subp$.
  %
  From the hypothesis that $\Gamma$ is reliable and
  Proposition~\ref{prop:env_subt_reliable} we deduce that
  $\Delta'$ is reliable.
  %
  We conclude by the induction hypothesis.

  \proofrule{t-guard}
  %
  Straightforward application of the induction hypothesis.

  \proofrule{t-fail}
  %
  This case is impossible because $E \not\subp \mathbb{0}$ and
  $\Gamma$ is reliable.

  \proofrule{t-free}
  %
  Then $P = \FreeuQ$ and
  $a : \ttqmarkE, \Gamma = u : \ttqmark\mathbb{1}, \Delta$
  and $\wtp\ContextBQ{}$.
  %
  From the hypotheses $\mathtt{M} \cdot F \subp E$
  and $F \not\subp \mathbb{0}$ we deduce $a \ne u$,
  hence $\Delta = a : \ttqmarkE, \Delta'$ for some
  $\Delta'$ such that $\Delta'$ is usable.
  %
  We conclude by the induction hypothesis.

  \proofrule{t-in}
  %
  Then $P = \Receiveu\Tag\seqof\VarXQ$ and
  $a : \ttqmarkE, \Gamma = u :
  \ttqmark(\tmessage\Tag\seqof\Type \cdot E'), \Delta$ and
  $\wtp{u : \ttqmarkE', \Delta, \seqof\VarX :
    \seqof\Type}Q{}$.
  %
  We distinguish the following sub-cases:
  \begin{itemize}
  \item Suppose $a = u$ and
    $\mathtt{M} \subp \tmessage\Tag\seqof\Type$.
    %
    Then $E = \tmessage\Tag\seqof\Type \cdot E'$.
    %
    From the hypotheses
    $\mathtt{M} \cdot F \subp E$ and
    $F \not\subp \mathbb{0}$ we deduce
    $E' \not\subp \mathbb{0}$.
    %
    We conclude by taking $\mathtt{M}' \stackrel{\text{\tiny def}}= \tmessage\Tag\seqof\Type$
    and $F' \stackrel{\text{\tiny def}}= E'$.
  \item Suppose $a = u$ and
    $\mathtt{M} \not\subp \tmessage\Tag\seqof\Type$.
    %
    From the hypotheses
    $\mathtt{M} \cdot F \subp E$ and
    $F \not\subp \mathbb{0}$ we deduce that
    $\mathtt{M} \cdot E'' \subp E'$ for some
    $E'' \not\subp \mathbb{0}$.
    %
    Observe that $\Delta = \Gamma$.
    %
    From the assumption that argument types are reliable we know
    that all the types in $\seqof\Type$ are reliable. Therefore we can
    conclude by the induction hypothesis.
  \item Suppose $a \ne u$.
    %
    From the hypothesis that $\Gamma$ is reliable we deduce
    $E' \not\subp \mathbb{0}$.
    %
    From the assumption that argument types are reliable we know
    that all the types in $\seqof\Type$ are reliable. Therefore we can
    conclude by the induction hypothesis.
  \end{itemize}

  \proofrule{t-branch}
  %
  Then $P = G_1 + G_2$ and
  $a : \ttqmarkE, \Gamma = u : \ttqmark(E_1 +
  E_2), \Delta$ and
  $\wtg{u : \ttqmarkE_i, \Delta}{G_i}$.
  %
  We distinguish two sub-cases:
  \begin{itemize}
  \item If $a = u$, then
    $E = E_1 + E_2$ and
    $\Gamma = \Delta$.
    %
    From the hypothesis
    $\mathtt{M} \cdot F \subp E$ we deduce
    $\mathtt{M} \cdot F \subp E_i$ for some
    $i=1,2$.\Luca{Questa proproet\`a richiede un lemma non banale
      che usa anche l'ipotesi che $E$ \`e in forma normale.}
    %
    We conclude by the induction hypothesis.
  \item If $a \ne u$, then
    $\Delta = a : \ttqmarkE, \Delta'$.
    %
    From the hypothesis that $\Gamma$ is reliable we deduce
    $E_1 + E_2 \not\subp \mathbb{0}$.
    %
    Suppose, without loss of generality, that
    $E_1 \not\subp \mathbb{0}$.  We conclude by applying the
    induction hypothesis on $G_1$.
    %
    \qedhere
  \end{itemize}
\end{proof}

\begin{lemma}
  \label{lem:termination}
  If $\wtp\EmptyContextP\psi$ and $P \arrownot\red$,
  then $P \equiv \mkkeyword{done}$.
\end{lemma}
\begin{proof}
  Using the hypothesis $P \arrownot\red$ and the laws of structural
  congruence we deduce that
  \[
    P \equiv \New\seqof\MailboxAQ
    \qquad
    \text{where}
    \qquad
    Q =
    \prod_{i\in I} \Send{a_i}{\Tag_i}{\seqof\MailboxC_i}
    \mathbin\ttbar
    \prod_{\mathclap{j\in J}}
    G_j
  \]
  where $\wtp{\seqof\MailboxA : \ttqmark\mathbb{1}}{Q}{\varphi}$ and
  $\varphi$ is acyclic and each guarded process $G_j$ concerns
  some mailbox $a_j$.
  %
  We prove the result by contradiction, assuming that
  $I \cup J \ne \emptyset$. The proof proceeds in two steps. In the
  first step we show that, for every $m\in I\cup J$, there exist
  $n\in I\cup J$ such that
  $\varphi \Rightarrow \gedge{a_n}{a_m}$ and $\varphi$
  contains an edge where $a_n$ and $a_m$ occur
  precisely in this order. In the second step, we show that this
  ultimately leads to a cyclic graph.

  Suppose $Q \equiv R \mathbin\ttbar G$ where
  $G \equiv \sum_{h\in H}
  \Receivea{\Tag_h}{\seqof\VarX_h}P_h\set{{} +
    \FreeaP'}$.
  %
  From \refrule{t-sub} and \refrule{t-par} we deduce that there
  exist $\Gamma_1$, $\Gamma_2$, $E$, $F$,
  $\varphi_1$ and $\varphi_2$ such that:
  \begin{itemize}
  \item
    $\wtp{\Gamma_1, a : \ttemarkE}R{\varphi_1}$
  \item
    $\wtp{\Gamma_2, a : \ttqmark(E \cdot
      F)}G{\varphi_2}$
  \item $\mathbb{1} \subp F$
  \end{itemize}
  where $\Gamma_1$ and $\Gamma_2$ are both reliable.
  %
  From \refrule{t-sub} and \refrule{t-guard} we deduce that
  $E \cdot F \subp \sum_{h\in H}
  \tmessage{\Tag_h}{\seqof\Type_h} \cdot E_h\set{{} +
    \mathbb{1}}$.
  %
  From Lemma~\ref{lem:output_occurrence} we deduce that there exist
  $n\geq 0$ and $F_1, \dots, F_n$ such that
  $F_1 \cdots F_n \subp E$ and
  $a^{\ttemarkF_k} \in R$ for all
  $1\leq k\leq n$.
  %
  Suppose $n = 0$. Then $\mathbb{1} \subp E$ and therefore
  $\mathbb{1} \subp E \cdot F$, meaning that the
  $\FreeaP'$ sub-term must be present in
  $G$. This is absurd for we know that $P \arrownot\red$, hence
  there must be at least one occurrence of $a$ in
  $R$.
  %
  In particular, one of the $F_k$ for $1\leq k\leq n$
  generates a non-empty subset of the $\tmessage{\Tag_h}{\seqof\Type_h}$
  for $h\in H$.
  %
  We reason by cases on the places where the
  $a^{\ttemarkF_k}$ may occur:
  \begin{itemize}
  \item From the hypothesis $P \arrownot\red$ we deduce that for
    every $i\in I$ either $a_i \ne a$ or
    $\Tag_i \ne \Tag_h$ for every $h\in H$. Therefore, the
    $a^{\ttemarkF_k}$ cannot be any of the $a_i$.
  %
  \item If $a^{\ttemarkF_k}$ occurs in
    $\set{\seqof\MailboxC_i}$ for some $i\in I$, then
    $a_i \ne a$ and
    $\varphi \Rightarrow \gedge{a_i}{a}$.
  \item All of the $a_j$ have an input capability, therefore
    the $a^{\ttemarkF_k}$ cannot be any of them.
  \item If $a^{\ttemarkF_k}$ occurs in $G_j$ for
    some $j\in J$, then $a_j \ne a$ because $a$
    is already used for input in $G$, so we have
    $\varphi \Rightarrow \gedge{a_j}{a}$.
  \end{itemize}

  Suppose
  $Q \equiv \Senda\Tag\seqof\MailboxC \mathbin\ttbar R$.
  %
  From \refrule{t-sub}, \refrule{t-par} and \refrule{t-msg} we
  deduce that there exist $\Gamma_1$, $\Gamma_2$, $E$,
  $F$, $\varphi_1$ and $\varphi_2$ such that:
  \begin{itemize}
  \item
    $\wtp{\Gamma_1, a :
      \ttemark\tmessage\Tag\seqof\Type}{\Senda\Tag\seqof\MailboxC}{\varphi_1}$
  \item
    $\wtp{\Gamma_2, a : \ttqmark(E \cdot
      F)}R{\varphi_2}$
  \item $\tmessage\Tag\seqof\Type \subp E$ and
    $\mathbb{1} \subp F$
  \end{itemize}
  where $\Gamma_1$ and $\Gamma_2$ are both reliable.
  %
  From Lemma~\ref{lem:input_occurrence} we deduce that there exist
  $\mathtt{M}$ and $F'$ such that
  $\tmessage\Tag\seqof\Type \subp \mathtt{M}$ and
  $F' \not\subp \mathbb{0}$ and
  $a^{\ttqmark\mathtt{M} \cdot F'} \in R$.
  %
  We reason by cases on the places where
  $a^{\ttqmark\mathtt{M} \cdot F'}$ may occur:
  %
  \begin{itemize}
  \item All the $a_i$ have an output capability, therefore
    $a^{\ttqmark\mathtt{M}\tmulF'}$ cannot be any of
    them.
  \item If $a^{\ttqmark\mathtt{M}\tmulF'}$ occurs in
    $\set{\seqof\MailboxC_i}$ for some $i\in I$, then
    $a_i \ne a$ and
    $\varphi \Rightarrow \gedge{a_i}{a}$.
  \item If $a^{\ttqmark\mathtt{M}\tmulF'} \in G_j$
    where $a_j \ne a$, then
    $\varphi \Rightarrow \gedge{a_j}{a}$.
  \item If
    $a^{\ttqmark\mathtt{M}\tmulF'} \in G_j \equiv
    \sum_{h\in H} \Receivea{\Tag_h}{\seqof\VarX_h}P_h\set{{}
      + \FreeaP'}$, then we can reason as in the
    case for inputs and find some $a_k \ne a$ such
    that $\varphi \Rightarrow \gedge{a_k}a$.
  \end{itemize}

  In summary, we have seen that starting from the assumption that
  $I \cup J \ne \emptyset$ it is possible to obtain a set $A$ of
  mailbox names that contains at least two distinct elements and
  such that for every $a \in A$ there exists
  $b \in A$ such that
  $\varphi \Rightarrow \gedge\MailboxBa$ and $\varphi$
  contains an edge where $b$ and $a$ precisely occur
  in this order. The set $A$ is necessarily finite because
  $Q$ is finite, therefore $\grel\varphi$ must be reflexive,
  which contradicts the hypothesis that $\varphi$ is acyclic. This
  is absurd, hence we conclude $I = J = \emptyset$.
\end{proof}

\begin{lemma}
  \label{lem:deadlock_freedom}
  If $\wtp\EmptyContextP\varphi$ and
  $P \rightarrow^* Q \arrownot\red$, then $Q \equiv \mkkeyword{done}$.
\end{lemma}
\begin{proof}
  Straightforward consequence of Theorem~\ref{thm:sr} and
  Lemma~\ref{lem:termination}.
\end{proof}

\section{Proofs of Theorems~\ref{thm:soundness} and~\ref{thm:fair_termination}}
\label{sec:proof_soundness}

\begin{reptheorem}{thm:soundness}
  If $\wtp\EmptyContextP\varphi$, then $P$ is
  mailbox conformant and deadlock free.
\end{reptheorem}
\begin{proof}
  Immediate consequence of Lemma~\ref{lem:conformance} and
  Lemma~\ref{lem:deadlock_freedom}.
\end{proof}

\begin{reptheorem}{thm:fair_termination}
  If $\wtp\EmptyContextP\varphi$ and $P$ is finitely
  unfolding, then $P$ is fairly terminating.
\end{reptheorem}
\begin{proof}
  Consider a reduction $P \rightarrow^* Q$. From the
  hypothesis that $P$ is finitely unfolding we know that
  there exists $R$ such that
  $P \rightarrow^* Q \rightarrow^* R$ and no reduction of
  $R$ uses \refrule{r-def}. We conclude applying
  Theorem~\ref{thm:sr} and Lemma~\ref{lem:fair_termination}.
\end{proof}

\input{proof_conformance}
\input{proof_deadlock_freedom}
\input{proof_termination}

\section{Proof of Theorem~\ref{thm:sr}}
\label{sec:proof_type_preservation}

\begin{lemma}
  \label{lem:subst}
  If $\wtp{\Gamma, \Var : \tau}P\varphi$ and
  $a \not\in\mathsf{dom}(\Gamma)$, then
  $\wtp{\Gamma, a :
    \tau}{P\substa\Var}{\varphi\substa\Var}$.
\end{lemma}
\begin{proof}
  A straightforward induction on the derivation of
  $\wtp{\Gamma, \Var : \tau}P\varphi$.
\end{proof}

\begin{lemma}
  If $\wtp\ContextP\varphi$ and
  $P \equiv Q$, then $\wtp\ContextQ\varphi$.
\end{lemma}
\begin{proof}
  An easy induction on the derivation of
  $P \equiv Q$, reasoning by cases on the last rule
  applied. The most critical points concern dependency graphs, whose
  structure changes as processes and restrictions are
  rearranged. Proposition~\ref{prop:grel} provides all the arguments
  to conclude that these changes do not affect the semantics of
  dependency graphs and therefore that no cycles are introduced.
\end{proof}

\begin{reptheorem}{thm:sr}
  If $\Gamma$ is reliable and $\wtp\ContextP\varphi$ and
  $P \rightarrow Q$, then
  $\wtp\ContextQ\varphi$.
\end{reptheorem}
\begin{proof}
  By induction on the derivation of $P \rightarrow Q$ and by
  cases on the last rule applied.

  \proofrule{r-read}
  %
  Then
  $P = \Senda\Tag\seqof\MailboxC \mathbin\ttbar
  \Receivea\Tag\seqof\VarXP + G\rightarrow
  P\subst\seqof\MailboxC\seqof\VarX = Q$.
  %
  From \refrule{t-sub} and \refrule{t-par} we deduce that there
  exist $\Gamma_1$, $\Gamma_2$, $\varphi_1$ and $\varphi_2$ such
  that:
  \begin{itemize}
  \item $\Gamma \leqslant \Gamma_1 \mathbin{\|} \Gamma_2$
  \item $\varphi \Rightarrow \varphi_1 \sqcup \varphi_2$
  \item
    $\wtp{\Gamma_1}{\Senda\Tag{\seqof\MailboxC}}{\varphi_1}$
  \item
    $\wtp{\Gamma_2}{\Receivea\Tag\seqof\VarXP +
      G}{\varphi_2}$
  \end{itemize}

  From \refrule{t-sub} and \refrule{t-msg} we deduce that there
  exist $\seqof\TypeT$ such that:
  \begin{itemize}
  \item
    $\Gamma_1 \leqslant a : \ttemark{\tmessage\Tag\seqof\Type},
    \seqof\MailboxC : \seqof\Type$
  \item
    $\varphi_1 \Rightarrow \gedgea{\set\seqof\MailboxC}$
  \end{itemize}

  From \refrule{t-sub} and \refrule{t-guard} we deduce that there
  exist $\Delta$ and $E$ such that:
  \begin{itemize}
  \item $\Gamma_2 \leqslant a : \ttqmarkE, \Delta$
  \item
    $\wtg{a : \ttqmarkE,
      \Delta}{\Receivea\Tag\seqof\VarXP + G}$
  \item $\df{}E$
  \item $\varphi_2 \Rightarrow \gedgea{\mathsf{dom}(\Delta)}$
  \end{itemize}

  From \refrule{t-branch}, \refrule{t-in} and $\df{}E$ we
  deduce that there exist $\seqof\TypeS$, $F_1$, $F_2$
  and $\psi$ such that:
  \begin{itemize}
  \item
    $E = \tmessage\Tag\seqof\TypeS \cdot F_1 +
    F_2$
  \item
    $\wtp{a : \ttqmarkF_1, \Delta, \seqof\VarX :
      \seqof\TypeS}{P}{\psi}$
  \item $F_1 \eqp \pderE{\tmessage\Tag\seqof\TypeS}$
  \end{itemize}

  From the fact that $\varphi$ is acyclic and the properties of
  $\varphi_1$ and $\varphi_2$ we deduce that
  $\set\seqof\MailboxC \cap \mathsf{dom}(\Delta) = \emptyset$. Indeed,
  suppose by contradiction that
  $u \in \set\seqof\MailboxC \cap \mathsf{dom}(\Delta)$ and observe that
  $u$ cannot be $a$. Then
  $\varphi_1 \Rightarrow \gedgeau$ and
  $\varphi_2 \Rightarrow \gedge\Namea$, so
  $\varphi \Rightarrow \gedgea\Mailbox$ which is absurd.

  From the definition of subtype environment and of
  $\Gamma_1 \mathbin{\|} \Gamma_2$ we deduce that:
  \begin{itemize}
  \item $\Gamma_1 = a : \ttemarkE', \Gamma_1'$ where
    $\ttemarkE' \leqslant \ttemark{\tmessage\Tag\seqof\TypeT}$ and
    $\Gamma'_1 \leqslant \seqof\MailboxC : \seqof\TypeT$
  \item
    $\Gamma_2 = a : \ttqmark\parens{E' \cdot
      F'}, \Gamma_2'$ where
    $\ttqmark\parens{E' \cdot F'} \leqslant \ttqmarkE$ and
    $\Gamma_2' \leqslant \Delta$
  \end{itemize}

  From the definition of $\leqslant$, the precongruence and transitivity
  properties of $\subp$ we derive
  $\tmessage\Tag\seqof\TypeT \cdot F' \subp E' \cdot
  F' \subp E$.
  %
  From the hypothesis that $\Gamma$ is reliable we deduce
  $F' \not\subp \mathbb{0}$.
  %
  From Proposition~\ref{prop:subt_der_subt} and $\df{}E$ we
  deduce $\seqof\TypeT \leqslant \seqof\TypeS$ and
  $F' \subp \pderE{\tmessage\Tag\seqof\TypeS}$.
  %
  From Lemma~\ref{lem:subst} we deduce
  $\wtp{a : \ttqmarkF_1, \Delta, \seqof\MailboxC :
    \seqof\TypeS}{P\subst\seqof\MailboxC\seqof\VarX}{\psi\subst\seqof\MailboxC\seqof\VarX}$.\Luca{In
    questo punto serve sapere che in $\psi$ non possono
    comparire nomi arbitrari, $\seqof\MailboxC$ in particolare, per non
    generare cicli.}
  %
  To conclude we apply \refrule{t-sub} observing that
  $\Gamma \leqslant \Gamma_1 \mathbin{\|} \Gamma_2 = a :
  \ttqmarkF', (\Gamma_1' \mathbin{\|} \Gamma_2') \leqslant a :
  \ttqmarkF_1, \Delta, \seqof\MailboxC : \seqof\TypeS$ using
  Proposition~\ref{prop:cmul_subt} and the fact that
  $\set\seqof\MailboxC \cap \mathsf{dom}(\Delta) = \emptyset$.

  \proofrule{r-free}
  %
  Then
  $P = \Newa(\FreeaQ + G)
  \rightarrow Q$.
  %
  From \refrule{t-sub} and \refrule{t-new} we deduce that there
  exist $\Delta$ and $\psi$ such that:
  \begin{itemize}
  \item $\Gamma \leqslant \Delta$
  \item $\varphi \Rightarrow \Newa\psi$
  \item
    $\wtp{\Delta, a : \ttqmark\mathbb{1}}{\FreeaQ
      + G}{\psi}$.
  \end{itemize}

  From \refrule{t-sub} and \refrule{t-guard} we deduce that there
  exist $\Delta'$, $E$ and $\psi'$ such that:
  \begin{itemize}
  \item
    $\Delta, a : \ttqmark\mathbb{1} \leqslant \Delta', a :
    \ttqmarkE$
  \item
    $\wtg{\Delta', a : \ttqmarkE}{\FreeaQ
      + G}$
  \item $\psi \Rightarrow \gedgea{\mathsf{dom}(\Delta')}$.
  \end{itemize}

  From \refrule{t-branch} and \refrule{t-free} we deduce that there
  exists $\psi'$ such that
  $\wtp{\Delta'}{Q}{\psi'}$.
  %
  From the well formedness condition on judgments and the definition
  of $\leqslant$ for type environments, we know that
  $\mathsf{dom}(\psi') \subseteq \mathsf{dom}(\Delta') \subseteq
  \mathsf{dom}(\Delta) \subseteq \mathsf{dom}(\Gamma)$.
  %
  From the fact that $\psi$ implies a connected graph with
  domain $\seta \cup \mathsf{dom}(\Delta')$ we deduce
  $\varphi \Rightarrow \psi \Rightarrow \psi'$.
  %
  We conclude with one application of \refrule{t-sub}.

  \proofrule{r-def}
  %
  Then
  $P = \invoke\RecVar\seqof\MailboxC \rightarrow
  R\subst\seqof\MailboxC\seqof\VarX = Q$ where
  $\define\RecVar\seqof\VarXR$.
  %
  From \refrule{t-sub} and \refrule{t-def} we deduce that there
  exist $\seqof\Type$ and $\psi$ such that
  $\Gamma \leqslant \seqof\MailboxC : \seqof\Type$ and
  $\RecVar : (\seqof\VarX : \seqof\Type; \psi)$ and
  $\varphi \Rightarrow \psi\subst\seqof\MailboxC\seqof\VarX$.
  %
  From the hypothesis that all process definitions are well typed we
  know that $\wtp{\seqof\VarX : \seqof\Type}R{\psi}$.
  %
  From Lemma~\ref{lem:subst} we deduce
  $\wtp{\seqof\MailboxC :
    \seqof\Type}{R\subst\seqof\MailboxC\seqof\VarX}{\psi\subst\seqof\MailboxC\seqof\VarX}$.
  %
  To conclude we apply \refrule{t-sub}.

  \proofrule{r-par}
  %
  Then
  $P = P_1 \mathbin\ttbar P_2 \rightarrow P_1' \mathbin\ttbar
  P_2 = Q$ where $P_1 \rightarrow P_1'$.
  %
  From \refrule{t-sub} and \refrule{t-par} we deduce that there
  exist $\Gamma_1$, $\Gamma_2$, $\varphi_1$ and $\varphi_2$ such
  that $\wtp{\Gamma_i}{P_i}{\varphi_i}$ for $i=1,2$ where
  $\Gamma \leqslant \Gamma_1 \mathbin{\|} \Gamma_2$ and
  $\varphi \Rightarrow \varphi_1 \sqcup \varphi_2$.
  %
  From the hypothesis that $\Gamma$ is reliable and
  Proposition~\ref{prop:env_subt_reliable} we deduce that
  $\Gamma_1 \mathbin{\|} \Gamma_2$ is reliable.
  %
  From the assumption that types are usable and
  Proposition~\ref{prop:env_mul_reliable} we deduce that
  $\Gamma_1$ is reliable.
  %
  From the induction hypothesis we deduce
  $\wtp{\Gamma_1}{P_1'}{\varphi_1}$.
  %
  To conclude we apply \refrule{t-par} and then \refrule{t-sub}.

  \proofrule{r-new}
  %
  Then
  $P = \NewaP' \rightarrow \NewaP'' =
  Q$ where $P' \rightarrow P''$.
  %
  From \refrule{t-sub} and \refrule{t-new} we deduce that there
  exist $\Delta$ and $\psi$ such that
  $\wtp{\Delta, a : \ttqmark\mathbb{1}}{P'}{\psi}$ where
  $\Gamma \leqslant \Delta$ and
  $\varphi \Rightarrow \Newa\psi$.
  %
  From the hypothesis that $\Gamma$ is reliable and
  Proposition~\ref{prop:env_subt_reliable} we deduce that
  $\Delta$ is reliable and so is
  $\Delta, a : \ttqmark\mathbb{1}$.
  %
  From the induction hypothesis we deduce
  $\wtp{\Delta, a : \ttqmark\mathbb{1}}{P''}{\psi}$.
  %
  To conclude we apply \refrule{t-new} and then \refrule{t-sub}.
\end{proof}

\subsection{Fair termination for finitely unfolding processes}
\label{sec:proof_termination}

\begin{lemma}
  \label{lem:fair_termination}
  If $\wtp\EmptyContextP\varphi$ and no reduction of
  $P$ uses \refrule{r-def}, then $P \rightarrow^* \mkkeyword{done}$.
\end{lemma}
\begin{proof}
  Let $\mathsf{size}(P)$ be the function inductively defined by the
  following equations
  \[
    \begin{array}{rcl}
      \mathsf{size}(\mkkeyword{done}) = \mathsf{size}(\Failu) = \mathsf{size}(\Sendu\Tag\seqof\NameV) = \mathsf{size}(\invoke\RecVar\seqof\NameU) & \stackrel{\text{\tiny def}}= & 0
      \\
      \mathsf{size}(\FreeuQ) = \mathsf{size}(\Receiveu\Tag\seqof\VarXQ)
      & \stackrel{\text{\tiny def}}= & 1 + \mathsf{size}(Q)
      \\
      \mathsf{size}(G_1 + G_2) & \stackrel{\text{\tiny def}}= &
      \max\set{ \mathsf{size}(G_1), \mathsf{size}(G_2) }
      \\
      \mathsf{size}(P_1 \mathbin\ttbar P_2) & \stackrel{\text{\tiny def}}= &
      \mathsf{size}(P_1) + \mathsf{size}(P_2)
      \\
      \mathsf{size}(\NewaQ) & \stackrel{\text{\tiny def}}= & \mathsf{size}(Q)
    \end{array}
  \]
  and observe that $P \rightarrow Q$ implies
  $\mathsf{size}(Q) < \mathsf{size}(P)$ from the hypothesis that no
  reduction of $P$ uses \refrule{r-def}.  Then $P$
  is strongly normalizing and we conclude by
  Lemma~\ref{lem:deadlock_freedom}.
\end{proof}

\subsection{Properties of well-typed processes}
\label{sec:properties}

In this section we state the main properties enjoyed by well-typed
processes. As usual, subject reduction is instrumental for all of
the results that follow as it guarantees that typing is preserved by
reductions:

\begin{theorem}
  \label{thm:sr}
  If $\Gamma$ is reliable and $\wtp\ContextP\varphi$ and
  $P \rightarrow Q$, then $\wtp\ContextQ\varphi$.
\end{theorem}

Interestingly, Theorem~\ref{thm:sr} seems to imply that the types of
the mailboxes used by a process do not change.  In sharp contrast,
other popular behavioral typing disciplines (session types in
particular), are characterized by a subject reduction result in
which types reduce along with processes.
Theorem~\ref{thm:sr} also seems to contradict the observations made
earlier concerning the fact that the mailboxes used by a process may
have different types (Example~\ref{ex:lock_type}).
The type preservation guarantee assured by Theorem~\ref{thm:sr} can
be explained by recalling that the type environment $\Gamma$ in a
judgment $\wtp\ContextP\varphi$ already takes into account
the overall balance between the messages stored into and consumed
from the mailbox used by $P$ (see
Definition~\ref{def:cmul}). In light of this observation,
Theorem~\ref{thm:sr} simply asserts that well-typed processes are
steady state: they never produce more messages than those that are
consumed, nor do they ever try to consume more messages than those
that are produced.

A practically relevant consequence of Theorem~\ref{thm:sr} is that,
by looking at the type $\ttqmarkE$ of the mailbox $a$ used
by a guarded process $P$ (rule~\refrule{t-guard}), it is
possible to determine \emph{bounds} to the number of messages that
can be found in the mailbox as $P$ waits for a message to
receive.  In particular, if every configuration of $E$
contains at most $k$ atoms with tag $\Tag$, then at runtime
$a$ contains at most $\Tag$-tagged messages. As a special
case, a mailbox of type $\ttqmark\mathbb{1}$ is guaranteed to be empty and can
be statically deallocated. Note that the bounds may change after
$P$ receives a message. For example, a free lock is
guaranteed to have no $\Tag[release]$ messages in its mailbox, and
will have at most one when it is busy (see
Example~\ref{ex:lock_derivation}).

The main result concerns the soundness of the type system,
guaranteeing that well-typed (closed) processes are both mailbox
conformant and deadlock free:

\begin{theorem}
  \label{thm:soundness}
  If $\wtp\EmptyContextP\varphi$, then $P$ is
  mailbox conformant and deadlock free.
\end{theorem}

Fair termination and junk freedom are not guaranteed by our typing
discipline in general. The usual counterexamples include processes
that postpone indefinitely the use of a mailbox with a relevant
type. For instance, the $\Tag$ message in the well-typed process
$\Newa\parens{ \Senda\Tag{} \mathbin\ttbar
  \invoke\RecVara }$ where
$\define\RecVar\Var{\invoke\RecVar\Var}$ is never consumed because
$a$ is never used for an input operation.

Nevertheless, fair termination is guaranteed for the class of
finitely unfolding processes:

\begin{theorem}
  \label{thm:fair_termination}
  We say that $P$ is \emph{finitely unfolding} if all
  maximal reductions of $P$ use \refrule{r-def} finitely
  many times.  If $\wtp\EmptyContextP\varphi$ and
  $P$ is finitely unfolding, then $P$ is fairly
  terminating.
\end{theorem}

The class of finitely unfolding processes obviously includes all
finite processes (those not using process invocations) but also many
recursive processes. For example, every process of the form
$\Newa\parens{ \Senda\Tag{} \mathbin\ttbar \cdots \mathbin\ttbar
  \Senda\Tag{} \mathbin\ttbar \invoke\RecVara }$ where
$\RecVar(\Var) \triangleq \Receive\Var\Tag{}\invoke\RecVar\Var
+ \Free\Var\mkkeyword{done}$ is closed, well typed and finitely unfolding
regardless of the number of $\Tag$ messages stored in $a$,
hence is fairly terminating and junk free by
Theorem~\ref{thm:fair_termination}.

\subsection{Properties of dependency graphs}
\label{sec:prop_graphs}

\begin{proposition}[structure preserving transitions]
  The following properties hold:
  \begin{enumerate}
  \item If
    $\varphi_1 \sqcup \varphi_2 \greduv \varphi$, then
    $\varphi = \varphi_1' \sqcup \varphi_2'$ for some
    $\varphi_1'$ and $\varphi_2'$.
  \item If $\Newa\varphi \greduv \psi$, then
    $\psi = \Newa\varphi'$ for some $\varphi'$.
  \end{enumerate}
\end{proposition}
\begin{proof}
  A straightforward induction on the derivation of the transition.
\end{proof}

Because of the previous result, in the proofs that follow we only
consider transitions where the structure of the dependency graph is
preserved.

\begin{proposition}
  \label{prop:gred_left}
  If
  $\varphi_1 \sqcup \varphi_2 \greduv \varphi_1'
  \sqcup \varphi_2'$, then
  $(\psi \sqcup \varphi_1) \sqcup \varphi_2
  \greduv (\psi \sqcup \varphi_1') \sqcup
  \varphi_2'$.
\end{proposition}
\begin{proof}
  By induction on the derivation of
  $\varphi_1 \sqcup \varphi_2 \greduv \varphi_1'
  \sqcup \varphi_2'$ and by cases on the last rule applied. We
  omit the discussion of \refrule{g-right}, which is symmetric to
  \refrule{g-left}.

  \proofrule{g-left}
  %
  Then $\varphi_1 \greduv \varphi_1'$ and
  $\varphi_2 = \varphi_2'$.
  %
  We conclude by applying \refrule{g-right}, then \refrule{g-left}.

  \proofrule{g-trans}
  %
  Then
  $\varphi_1 \sqcup \varphi_2 \greduw \varphi_1''
  \sqcup \varphi_2'' \gred\NameWv \varphi_1' \sqcup
  \varphi_2'$.
  %
  Using the induction hypothesis we derive
  $(\psi \sqcup \varphi_1) \sqcup \varphi_2
  \greduw (\psi \sqcup \varphi_1'') \sqcup
  \varphi_2'' \gred\NameWv (\psi \sqcup \varphi_1')
  \sqcup \varphi_2'$ and we conclude with one application of
  \refrule{g-trans}.
\end{proof}

\begin{proposition}
  \label{prop:gred_gunion}
  If
  $\varphi_1 \sqcup (\varphi_2 \sqcup \varphi_3) \greduv
  \varphi_1' \sqcup (\varphi_2' \sqcup \varphi_3')$, then
  $(\varphi_1 \sqcup \varphi_2) \sqcup \varphi_3 \greduv
  (\varphi_1' \sqcup \varphi_2') \sqcup \varphi_3'$.
\end{proposition}
\begin{proof}
  By induction on the derivation of
  $\varphi_1 \sqcup (\varphi_2 \sqcup \varphi_3) \greduv
  \varphi_1' \sqcup (\varphi_2' \sqcup \varphi_3')$ and by cases
  on the last rule applied.

  \proofrule{g-left}
  %
  Then $\varphi_1 \greduv \varphi_1'$ and
  $\varphi_2 = \varphi_2'$ and $\varphi_3 = \varphi_3'$.
  %
  We conclude with two applications of \refrule{g-left}.

  \proofrule{g-right}
  %
  Then $\varphi_1 = \varphi_1'$ and
  $\varphi_2 \sqcup \varphi_3 \greduv \varphi_2' \sqcup
  \varphi_3'$.
  %
  We conclude by Proposition~\ref{prop:gred_left}.

  \proofrule{g-trans}
  %
  Then
  $\varphi_1 \sqcup (\varphi_2 \sqcup \varphi_3) \greduw
  \varphi_1'' \sqcup (\varphi_2'' \sqcup \varphi_3'')
  \gred\NameWv \varphi_1' \sqcup (\varphi_2' \sqcup
  \varphi_3')$.
  %
  Using the induction hypothesis we deduce
  $(\varphi_1 \sqcup \varphi_2) \sqcup \varphi_3 \greduw
  (\varphi_1'' \sqcup \varphi_2'') \sqcup \varphi_3''
  \gred\NameWv (\varphi_1' \sqcup \varphi_2') \sqcup
  \varphi_3'$.
  %
  We conclude with one application of \refrule{g-trans}.
\end{proof}

\begin{proposition}
  \label{prop:gred_new}
  If
  $\Newa\varphi_1 \sqcup \varphi_2 \greduv
  \Newa\varphi_1' \sqcup \varphi_2'$ and
  $a\not\in\mathsf{fn}(\varphi_2)$, then
  $\Newa(\varphi_1 \sqcup \varphi_2) \greduv
  \Newa(\varphi_1' \sqcup \varphi_2')$.
\end{proposition}
\begin{proof}
  By induction on the derivation of
  $\Newa\varphi_1 \sqcup \varphi_2 \greduv
  \Newa\varphi_1' \sqcup \varphi_2'$ and by cases on the
  last rule applied. We do not discuss rule \refrule{g-right}, which
  is straightforward.

  \proofrule{g-left}
  %
  Then
  $\Newa\varphi_1 \greduv \Newa\varphi_1'$
  and $\varphi_2 = \varphi_2'$.
  %
  From \refrule{g-new} we deduce
  $\varphi_1 \greduv \varphi_1'$ and
  $a\neu,v$.
  %
  We conclude with one application of \refrule{g-left} and one
  application of \refrule{g-new}.

  \proofrule{g-trans}
  %
  Then
  $\Newa\varphi_1 \sqcup \varphi_2 \greduw
  \Newa\varphi_1'' \sqcup \varphi_2'' \gred\NameWv
  \Newa\varphi_1' \sqcup \varphi_2'$.
  %
  From the induction hypothesis we deduce
  $\Newa(\varphi_1 \sqcup \varphi_2) \greduw
  \Newa(\varphi_1'' \sqcup \varphi_2'') \gred\NameWv
  \Newa(\varphi_1' \sqcup \varphi_2')$.
  %
  We conclude with one application of \refrule{g-trans}.
\end{proof}

\begin{proposition}
  \label{prop:grel}
  The following properties hold:
  \begin{enumerate}
  \item\label{item:grel_empty}
    $\grel{\emptyset \sqcup \varphi} = \grel\varphi$
  \item\label{item:grel_comm}
    $\grel{\varphi_1 \sqcup \varphi_2} = \grel{\varphi_2 \sqcup
      \varphi_1}$
  \item\label{item:grel_assoc}
    $\grel{\varphi_1 \sqcup (\varphi_2 \sqcup \varphi_3)} =
    \grel{(\varphi_1 \sqcup \varphi_2) \sqcup \varphi_3}$
  \item\label{item:grel_new} If $a\not\in\mathsf{fn}(\varphi_2)$,
    then
    $\grel{\Newa\varphi_1 \sqcup \varphi_2} =
    \grel{\Newa(\varphi_1 \sqcup \varphi_2)}$.
  \end{enumerate}
\end{proposition}
\begin{proof}
  Items~\ref{item:grel_empty} and~\ref{item:grel_comm} are trivial.
  Items~\ref{item:grel_assoc} and~\ref{item:grel_new} respectively
  follow from Proposition~\ref{prop:gred_gunion} and
  Proposition~\ref{prop:gred_new}.
\end{proof}

\subsection{Properties of subtyping}
\label{sec:prop_subtyping}

\begin{proposition}
  \label{prop:subt_reliable_usable}
  If $\tau \leqslant \sigma$, then $\tau$ reliable implies $\sigma$
  reliable and $\sigma$ usable implies $\tau$ usable.
\end{proposition}
\begin{proof}
  We only prove the part of the statement concerning reliability,
  since usability is analogous, and we prove the reverse implication.
  %
  The interesting case is when $\tau = \ttqmarkE$. From the
  hypothesis $\tau \leqslant \sigma$ we deduce $\sigma = \ttqmarkF$
  and $E \subp F$.
  %
  Now if $F \subp \mathbb{0}$ we have
  $E \subp F \subp \mathbb{0}$ by transitivity of
  $\subp$. Hence, $\sigma$ unreliable implies $\tau$ unreliable.
\end{proof}

\begin{proposition}
  \label{prop:subt_der_subt}
  If $\tmessage\Tag\seqof\TypeT \cdot F \subp E$ and
  $F \not\subp \mathbb{0}$ and
  $\pderE{\tmessage\Tag\seqof\TypeS}$ is defined, then
  $\seqof\TypeT \leqslant \seqof\TypeS$ and
  $F \subp \pderE{\tmessage\Tag\seqof\TypeS}$.
\end{proposition}
\begin{proof}
  Let $\mathsf{A} \in \sem{\tmessage\Tag\seqof\TypeT \cdot F}$.
  %
  From the hypothesis $F \not\subp \mathbb{0}$ we deduce that
  $\mathsf{A} = \bag{\tmessage\Tag\seqof\TypeT} \uplus \bag[i\in
  I]{\tmessage{\Tag_i}{\seqof\TypeT_i}}$ where
  $\bag[i\in I]{\tmessage{\Tag_i}{\seqof\TypeT_i}} \in \semF$.
  %
  From the hypothesis
  $\tmessage\Tag\seqof\TypeT \cdot F \subp E$ and the
  definition of $\subp$ we deduce that there exist $\seqof\TypeR$ and
  $\seqof\TypeR_i$ such that
  $\bag{\tmessage\Tag\seqof\TypeR} \uplus \bag[i\in
  I]{\tmessage{\Tag_i}{\seqof\TypeR_i}} \in \semE$ and
  $\seqof\TypeT \leqslant \seqof\TypeR$ and $\seqof\TypeT_i \leqslant \seqof\TypeR_i$ for every
  $i\in I$.
  %
  From the hypothesis that $\pderE{\tmessage\Tag\seqof\TypeS}$ is
  defined we deduce that $\seqof\TypeR \leqslant \seqof\TypeS$, hence
  $\seqof\TypeT \leqslant \seqof\TypeS$.
  %
  Also, from the definition of derivative, we have
  $\bag[i\in I]{\tmessage{\Tag_i}{\seqof\TypeR_i}} \in
  \sem{\pderE{\tmessage\Tag\seqof\TypeS}}$.
  %
  We conclude
  $F \subp \pderE{\tmessage\Tag\seqof\TypeS}$.
\end{proof}

We extend the terminology used for type classification
(Definition~\ref{def:classification}) to type environments as
well. We say that $\Gamma$ is reliable/irrelevant if all the types
in its range are reliable/irrelevant.

\begin{example}
  \label{ex:global_assumptions}
  The global assumptions we made on types are aimed at ensuring that
  in a judgment $\wtp{u : \tau, \Gamma}P{}$ where
  $\tau$ is relevant and $\Gamma$ is reliable the name $u$
  does indeed occur free in $P$.
  %
  If we allowed unreliable arguments, then it would be possible to
  derive
  \[
    \wtp{
      u : \tau,
      v : \ttqmark\tmessage\Tag{\ttqmark\mathbb{0}}
    }{
      \Receivev\Tag\Var
      \Fail\Var
    }{
      \emptyset
    }
  \]
  meaning that $u$ is not guaranteed to occur even if $\tau$
  is relevant.
  %
  Analogously, if we allowed unusable arguments, then it would be
  possible to derive
  \[
    \wtp{
      u : \tau,
      v : \ttemark\tmessage\Tag{\ttemark\mathbb{0}}
    }{
      \Newa\parens{
        \Sendv\Taga
        \mathbin\ttbar
        \Faila
      }
    }{
      \Newa\gedge\NameVa
    }
  \]
  again meaning that $u$ is not guaranteed to occur even if
  $\tau$ is relevant.
  %
  \hfill$\blacksquare$
\end{example}

\subsection{Properties of type environments}
\label{sec:prop_type_environments}

\begin{proposition}
  \label{prop:env_subt_reliable}
  If $\Gamma \leqslant \Delta$, then $\Gamma$ reliable implies
  $\Delta$ reliable and $\Delta$ usable implies $\Gamma$
  usable.
\end{proposition}
\begin{proof}
  Immediate from Proposition~\ref{prop:subt_reliable_usable}.
\end{proof}

\begin{proposition}
  \label{prop:cmul_subt}
  If both $\Gamma_1 \mathbin{\|} \Gamma_2$ and
  $\Delta_1, \Delta_2$ are defined and
  $\Gamma_i \leqslant \Delta_i$, then
  $\Gamma_1 \mathbin{\|} \Gamma_2 \leqslant \Delta_1, \Delta_2$.
\end{proposition}
\begin{proof}
  We discuss a few notable cases when
  $u \in (\mathsf{dom}(\Gamma_1) \cap \mathsf{dom}(\Gamma_2) \cap
  \mathsf{dom}(\Delta_1)) \setminus \mathsf{dom}(\Delta_1)$.

  \proofcase{$\Gamma_1(u) = \ttemarkE$ and
    $\Gamma_2(u) = \ttemarkF$ and
    $\Delta_1(u) = \ttemarkG$}
  %
  Then $\ttemarkE \leqslant \ttemarkG$ and
  $\ttemarkF \leqslant \ttemark\mathbb{1}$, which means
  $G \subp E$ and $\mathbb{1} \subp F$.
  %
  From the properties of $\subp$ we deduce
  $G \subp G \cdot \mathbb{1} \subp E \cdot
  F$.
  %
  We conclude
  $(\Gamma_1 \mathbin{\|} \Gamma_2)(u) = \ttemark\parens{E
    \cdot F} \leqslant \ttemarkG = (\Delta_1,
  \Delta_2)(u)$.

  \proofcase{$\Gamma_1(u) = \ttemarkE$ and
    $\Gamma_2(u) = \ttqmark\parens{E \cdot F}$
    and $\Delta_1(u) = \ttemarkG$}
  %
  Then $\ttemarkE \leqslant \ttemarkG$ and
  $\ttqmark\parens{E \cdot F} \leqslant \ttemark\mathbb{1}$, which
  means $G \subp E$ and
  $E \cdot F \cdot \mathbb{1} \subp E \cdot
  F \subp \mathbb{1}$.
  %
  From the properties of $\subp$ we deduce
  $G \subp E \subp \mathbb{1}$ and
  $F \subp \mathbb{1}$.
  %
  We conclude
  $\parens{\Gamma_1 \mathbin{\|} \Gamma_2}(u) = \ttqmarkF \leqslant
  \ttemarkG = (\Delta_1, \Delta_2)(u)$.

  \proofcase{$\Gamma_1(u) = \ttqmark\parens{E \cdot
      F}$ and $\Gamma_2(u) = \ttemarkE$ and
    $\Delta_1(u) = \ttqmarkG$}
  %
  Then $\ttqmark\parens{E \cdot F} \leqslant \ttqmarkG$
  and $\ttemarkE \leqslant \ttemark\mathbb{1}$, which means
  $E \cdot F \subp G$ and
  $\mathbb{1} \subp E$.
  %
  From the properties of $\subp$ we deduce
  $F \subp \mathbb{1} \cdot F \subp E \cdot
  F \subp G$.
  %
  We conclude
  $\parens{\Gamma_1 \mathbin{\|} \Gamma_2}(u) = \ttqmarkF
  \leqslant \ttqmarkG = (\Delta_1, \Delta_2)(u)$.

  \proofcase{$\Gamma_1(u) = \ttqmark\parens{E \cdot
      F}$ and $\Gamma_2(u) = \ttemarkE$ and
    $\Delta_1(u) = \ttemarkG$}
  %
  Then $\ttqmark(E \cdot F) \leqslant \ttemarkG$ and
  $\ttemarkE \leqslant \ttemark\mathbb{1}$, which means
  $E \cdot F \cdot G \subp \mathbb{1}$ and
  $\mathbb{1} \subp E$.
  %
  From the properties of $\subp$ we deduce
  $F \cdot G \subp \mathbb{1}$.
  %
  We conclude
  $\parens{\Gamma_1 \mathbin{\|} \Gamma_2}(u) = \ttqmarkF
  \leqslant \ttemarkG = (\Delta_1, \Delta_2)(u)$.
\end{proof}

\begin{proposition}
  \label{prop:env_mul_reliable}
  If $\Gamma$ is usable and $\Gamma \mathbin{\|} \Delta$ is
  reliable, then $\Delta$ is reliable.
\end{proposition}
\begin{proof}
  We discuss only the interesting case when
  $\Gamma(u) = \ttemarkE$ and
  $\Delta(u) = \ttqmark(E \cdot F)$, the others
  being symmetric or simpler.
  %
  Then $(\Gamma \mathbin{\|} \Delta)(u) = \ttqmarkF$.
  %
  From the hypothesis that $\Gamma$ is usable we deduce
  $\ttemark\mathbb{0} \not\leqslant \ttemarkE$, that is
  $E \not\subp \mathbb{0}$.
  %
  From the hypothesis that $\Gamma \mathbin{\|} \Delta$ is reliable
  we deduce $\ttqmarkF \not\leqslant \ttqmark\mathbb{0}$, that is
  $F \not\subp \mathbb{0}$.
  %
  We conclude $E \cdot F \not\subp \mathbb{0}$.
\end{proof}

\section{Related Work}
\label{sec:related}

\subparagraph*{Concurrent Objects.}
There are analogies between actors and concurrent objects. Both
entities are equipped with a unique identifier through which they
receive messages, they may interact with several concurrent clients
and their behavior may vary over time, as the entity interacts with
its clients. Therefore, static analysis techniques developed for
concurrent objects may be applicable to actors (and vice versa).
Relevant works exploring behavioral type systems for concurrent
objects include those of Najim \emph{et al.}\xspace~\cite{NajmNimourStefani99},
Ravara and Vasconcelos~\cite{RavaraVasconcelos00}, and Puntigam
\emph{et al.}\xspace~\cite{Puntigam01,PuntigamPeter01}.
As in the pure actor model, each object has a unique mailbox and the
input capability on that mailbox cannot be transferred. The mailbox
calculus does not have these constraints. A notable variation is the
model studied by Ravara and Vasconcelos~\cite{RavaraVasconcelos00},
which accounts for \emph{distributed objects}: there can be several
copies of an object that react to messages targeted to the same
mailbox.
Another common trait of these works is that the type discipline
focuses on sequences of method invocations and types contain
(abstract) information on the internal state of objects and on state
transitions. Indeed, types are either finite-state
automata~\cite{NajmNimourStefani99}, or terms of a process
algebra~\cite{RavaraVasconcelos00} or tokens annotated with state
transitions~\cite{PuntigamPeter01}.
In contrast, mailbox types focus on the content of a mailbox and
sequencing is expressed in the type of explicit continuations.
The properties enforced by the type systems in these works differ
significantly. Some do not consider deadlock
freedom~\cite{RavaraVasconcelos00,Puntigam01}, others do not account
for out-of-order message processing~\cite{Puntigam01}.
Details on the enforced properties also vary. For example, the
notion of protocol conformance used by Ravara and
Vasconcelos~\cite{RavaraVasconcelos00} is such that any message sent
to an object that is unable to handle that message, but can do so in
some future state is accepted. In our setting, this would mean
allowing to send a $\Tag[release]$ message to a free lock if the lock
is acquired later on, or allowing to send a $\Tag[reply]$ message to
an account if the account will later be involved in a transaction.

The most closely related work among those addressing concurrent
objects is the one by Crafa and Padovani~\cite{CrafaPadovani17}, who
propose the use of the Objective Join Calculus as a model for
non-uniform, concurrent objects and develop a type discipline that
can be used for enforcing concurrent object protocols.  Mailbox
types have been directly inspired by their types of concurrent
objects.
There are two main differences between the work of Crafa and
Padovani~\cite{CrafaPadovani17} and our own.
First, in the Objective Join Calculus every object is associated
with a single mailbox, just like in the pure actor
model~\cite{HewittEtAl73,Agha86}, meaning that mailboxes are not
first class. As a consequence, the types considered by Crafa and
Padovani~\cite{CrafaPadovani17} all have an (implicit) output
capability.
Second, in the Objective Join Calculus input operations are defined
atomically on molecules of messages, whereas in the mailbox calculus
messages are received one at a time. As a consequence, the type of a
mailbox in the work of Crafa and Padovani~\cite{CrafaPadovani17} is
invariant, whereas the same mailbox may have different types at
different times in the mailbox calculus
(Example~\ref{ex:lock_type}). Remarkably, this substantial
difference has no impact on the structure of the type language that
we consider.

\subparagraph*{Static analysis of actors.}
Srinivasan and Mycroft~\cite{SrinivasanMycroft08} define a type
discipline for controlling the ownership of messages and ensuring
actor isolation, but consider only uniformly typed mailboxes and do
not address mailbox conformance or deadlock freedom.

Christakis and Sagonas~\cite{ChristakisSagonas11} describe a static
analysis technique whose aim is to ensure matching between send and
receive operations in actors.  The technique, which is described
only informally and does not account for deadlocks, has been
implemented in a tool called \textsf{dialyzer} and used for the
analysis of Erlang programs.

Crafa~\cite{Crafa12} defines a behavioural type system for actors
aimed at ensuring that the order of messages produced and consumed
by an actor follows a prescribed protocol. Protocols are expressed
as types and describe the behavior of actors rather than the content
of the mailboxes they use. Deadlock freedom is not addressed.

Charousset \emph{et al.}\xspace~\cite{CharoussetHiesgenSchmidt16} describe the
design and implementation of CAF, the C++ Actor Framework. Among the
features of CAF is the use of \emph{type-safe message passing
  interfaces} that makes it possible to statically detect a number
of protocol violations by piggybacking on the C++ type system. There
are close analogies between CAF's message passing interfaces and
mailbox types with output capability: both are equipped with a
subset semantics and report only those messages that can be stored
into the mailbox through a mailbox reference with that type.
Charousset \emph{et al.}\xspace~\cite{CharoussetHiesgenSchmidt16} point out that
this feature fosters the decoupling of actors and enables
incremental program recompilation.

Giachino \emph{et al.}\xspace~\cite{GiachinoEtAl16,Mastandrea16} define a type
system for the deadlock analysis of actors making use of implicit
futures. Mailbox conformance and deadlocks due to communications are
not taken into account.

Fowler \emph{et al.}\xspace~\cite{FowlerLindleyWadler17} formalize channel-based
and mailbox-based communicating systems, highlighting the
differences between the two models and studying type-preserving
encodings between them. Mailboxes in their work are uniformly typed,
but the availability of union types make it possible to host
heterogeneous values within the same mailbox. This however may lead
to a loss of precision in typing. This phenomenon, dubbed \emph{type
  pollution} by Fowler \emph{et al.}\xspace~\cite{FowlerLindleyWadler17}, is
observable to some extent also in our typing discipline and can be
mitigated by the use of multiple mailboxes (\emph{cf.}\xspace
Section~\ref{sec:example_master_workers}).
Finally, Fowler \emph{et al.}\xspace~\cite{FowlerLindleyWadler17} leave the
extension of their investigation to behaviorally-typed language of
actors as future work. Our typing discipline is a potential
candidate for this investigation and addresses a more general
setting thanks to the support for first-class mailboxes.

\subparagraph*{Sessions and actors.}
The encoding of binary sessions into actors discussed in
Section~\ref{sec:example_binary_sessions} is new and has been
inspired by the encoding of binary sessions into the linear
$\pi$-calculus~\cite{Kobayashi07,DardhaGiachinoSangiorgi17}, whereby
each message is paired with a continuation. In our case, the
continuation, instead of being a fresh (linear) channel, is either
the mailbox of the peer or that of the session. This style of
communication with explicit continuation passing is idiomatic in the
actor model, which is based on asynchronous communications.
The encoding discussed in Section~\ref{sec:example_binary_sessions}
can be generalized to multiparty sessions by defining
$\SessionProcessT$ as a \emph{medium process} through
which messages are exchanged between the parties of the
session. This idea has been put forward by Caires and
P\'erez~\cite{CairesPerez16} to encode multiparty sessions using
binary sessions.

Mostrous and Vasconcelos~\cite{MostrousVasconcelos11} study a
session type system for enforcing ordered dyadic interactions in
core Erlang. They use \emph{references} for distinguishing messages
pertaining to different sessions, making use of the advanced pattern
matching capabilities of Erlang. Their type system guarantees a
weaker form of mailbox conformance, whereby junk messages may be
present at the end of a computation, and does not consider deadlock
freedom. Compared to our encoding of binary sessions, their approach
does not require a medium process representing the session itself.

Neykova and Yoshida~\cite{NeykovaYoshida16} propose a framework
based on multiparty session types for the specification and
implementation of actor systems with guarantees on the order of
interactions. This approach is applicable when designing an entire
system and both the network topology and the communication protocol
can be established in advance.
Fowler~\cite{Fowler16} builds upon the work of Neykova and Yoshida
to obtain a runtime protocol monitoring mechanism for Erlang.
Charalambides \emph{et al.}\xspace~\cite{CharalambidesDingesAgha16} extend the
multiparty session approach with a protocol specification language
that is parametric in the number of actors participating in the
system.
In contrast to these approaches based on multiparty/global session
types, our approach ensures mailbox conformance and deadlock freedom
of a system compositionally, as the system is assembled out of
smaller components, and permits the modeling of systems with a
dynamic network topology or with a varying number of interacting
processes.

\subparagraph*{Linear logic.}
Shortly after its introduction, linear logic has been proposed as a
specification language suitable for concurrency.
Following this idea, Kobayashi and
Yonezawa~\cite{KobayashiYonezawa94,KobayashiYonezawa95} have studied
formal models of concurrent objects and actors based on linear
logic. More recently, a direct correspondence between propositions
of linear logic and session types has been
discovered~\cite{CairesPfenning10,Wadler14,LindleyMorris15}.
There are several analogies between the mailbox type system and the
proof system of linear logic.
Mailbox types with output capability are akin to positive
propositions, with $\ttemark\mathbb{0}$ and $\ttemark\mathbb{1}$ respectively playing
the roles of $0$ and $1$ in linear logic and
$\ttemark(E + F)$ and
$\ttemark(E \cdot F)$ corresponding to $\oplus$ and
$\otimes$. Mailbox types with input capability are akin to negative
propositions, with $\ttqmark\mathbb{0}$ and $\ttqmark\mathbb{1}$ corresponding to
$\top$ and $\bot$ and $\ttqmark(E + F)$ and
$\ttqmark(E \cdot F)$ corresponding to $\with$ and
$\parr$.
Rules~\refrule{t-fail}, \refrule{t-free} and \refrule{t-branch} have
been directly inspired from the rules for $\top$, $\bot$ and $\with$
in the classical sequent calculus for linear logic.
Subtyping corresponds to inverse linear implication and its
properties are consistent with those of the logic connectives
according to the above interpretation.
A noteworthy difference between our type system and those for
session types based on linear
logic~\cite{CairesPfenning10,Wadler14,LindleyMorris15} is the need
for dependency graphs to ensure deadlock freedom
(Section~\ref{sec:graphs}). There are two reasons that call for such
auxiliary mechanism in our setting. First, the rule \refrule{t-par}
is akin to a symmetric cut rule. Dependency graphs are necessary to
detect mutual dependencies that may consequently arise
(Example~\ref{ex:future_deadlock}). Second, unlike session endpoints
that are linear resources, mailbox references can be used
non-linearly. Thus, the multiplicity of dependencies, and not just
the presence or absence thereof, is relevant
(Example~\ref{ex:multiplicity}).

\subsection{Typing Rules}
\label{sec:rules}

\begin{table}
  \begin{center}
    \[
      \begin{array}{@{}c@{}}
        \multicolumn{1}{@{}l@{}}{\textbf{Typing rules for processes}\hfill\framebox{$\wtp\ContextP{\smash\varphi}$}}
        \\\\
        \inferrule{

        }{
          \wtp\emptyset\mkkeyword{done}\emptyset
        }
        ~~\defrule{t-done}
        \qquad
        \inferrule{
          \RecVar : (\seqof\VarX : \seqof\Type; \varphi)

        }{
          \wtp{
            \seqof\NameU : \seqof\Type
          }{
            \invoke\RecVar\seqof\NameU
          }{
            \varphi\subst\seqof\NameU\seqof\VarX
          }
        }
        ~~\defrule{t-def}
        \qquad
        \inferrule{
          \wtp{\Gamma, a : \ttqmark\mathbb{1}}P\varphi
        }{
          \wtp\Gamma{\NewaP}{\Newa\varphi}
        }
        ~~\defrule{t-new}
        \\\\
        \inferrule{

        }{
          \wtp{
            u : \ttemark{\tmessage\Tag\seqof\TypeT},
            \seqof\NameV : \seqof\TypeT
          }{
            \Sendu\Tag\seqof\NameV
          }{
            \gedgeu{\set\seqof\NameV}
          }
        }
        ~~\defrule{t-msg}
        \qquad
        \inferrule{
          \wtg{
            u : \ttqmarkE,
            \Gamma
          }{
            G
          }
          \\
          \vDash E
        }{
          \textstyle
          \wtp{
            u : \ttqmarkE,
            \Gamma
          }{
            G
          }{
            \gedgeu{\mathsf{dom}(\Gamma)}
          }
        }
        ~~\defrule{t-guard}
        \\\\
        \inferrule{
          \wtp{\Gamma_i}{P_i}{\varphi_i}~{}^{(i=1,2)}
        }{
          \wtp{
            \Gamma_1 \mathbin{\|} \Gamma_2
          }{
            P_1 \mathbin\ttbar P_2
          }{
            \varphi_1 \sqcup \varphi_2
          }
        }
        ~~\defrule{t-par}
        \qquad
        \inferrule{
          \wtp\ContextBP\psi
          \\
          \Gamma \leqslant \Delta
          \\
          \varphi \Rightarrow \psi
        }{
          \wtp\ContextAP\varphi
        }
        ~~\defrule{t-sub}
        \\\\
        \multicolumn{1}{@{}l@{}}{\textbf{Typing rules for guards}\hfill\framebox{$\wtg\ContextG$}}
        \\\\
        \inferrule{

        }{
          \wtg{
            u : \ttqmark\mathbb{0},
            \Gamma
          }{
            \Failu
          }
        }
        ~~\defrule{t-fail}
        \qquad
        \inferrule{
          \wtp\ContextP\varphi
        }{
          \wtg{
            u : \ttqmark\mathbb{1}, \Gamma
          }{
            \FreeuP
          }
        }
        ~~\defrule{t-free}
        \\\\
        \inferrule{
          \wtp{
            u : \ttqmarkE,
            \Gamma,
            \seqof\VarX : \seqof\Type
          }{
            P
          }{
            \varphi
          }

        }{
          \wtg{
            u : \ttqmark(\tmessage\Tag\seqof\Type\tmulE),
            \Gamma
          }{
            \Receiveu\Tag\seqof\VarXP
          }
        }
        ~~\defrule{t-in}
        \qquad
        \inferrule{
          \wtg{
            u : \ttqmarkE_i,
            \Gamma
          }{
            G_i
          }
          ~{}^{(i=1,2)}
        }{
          \wtg{
            u : \ttqmark(E_1 + E_2),
            \Gamma
          }{
            G_1 + G_2
          }
        }
        ~~\defrule{t-branch}
      \end{array}
    \]
  \end{center}
  \caption{
    \label{tab:inference}
    Typing rules.
  }
\end{table}

We use \emph{type environments} for tracking the type of free names
occurring in processes. A type environment is a partial function
from names to types written as $\seqof\NameU : \seqof\Type$ or
$u_1 : \tau_1, \dots, u_n : \tau_n$. We let $\Gamma$ and
$\Delta$ range over type environments, we write $\mathsf{dom}(\Gamma)$ for
the domain of $\Gamma$ and $\Gamma, \Delta$ for the union of
$\Gamma$ and $\Delta$ when
$\mathsf{dom}(\Gamma) \cap \mathsf{dom}(\Delta) = \emptyset$.
We say that $\Gamma$ is reliable if so are all the types in its
range.

Judgments for processes have the form $\wtp\ContextP\varphi$,
meaning that $P$ is well typed in $\Gamma$ and yields the
dependency graph $\varphi$. Judgments for guards have the form
$\wtg\ContextG$, meaning that $G$ is well typed in
$\Gamma$.
We say that a judgment $\wtp\ContextP\varphi$ is well formed
if $\mathsf{fn}(\varphi) \subseteq \mathsf{dom}(\Gamma)$\Luca{Se si toglie
  l'entailment da \refrule{t-sub} questa condizione non serve pi\`u
  e si semplificano le regole e la descrizione. Considerare questa
  modifica dopo aver ricontrollato le prove.} and $\varphi$ is
acyclic.  Each process typing rule has an implicit side condition
requiring that its conclusion is well formed.
For each global process definition $\define\RecVar\seqof\VarXP$ we
assume that there is a corresponding \emph{global process
  declaration} of the form $\RecVar : (\seqof\VarX : \seqof\Type; \varphi)$.
We say that the definition is \emph{consistent} with the
corresponding declaration if $\wtp{\seqof\VarX : \seqof\Type}P\varphi$.
Hereafter, all process definitions are assumed to be consistent.
We now discuss the typing rules in detail, introducing auxiliary
notions and notation as we go along.

\DiscussRule{Terminated process}
According to the rule \refrule{t-done}, the terminated process
$\mkkeyword{done}$ is well typed in the empty type environment and yields no
dependencies. This is motivated by the fact that $\mkkeyword{done}$ does not
use any mailbox. Later on we will introduce a subsumption rule
\refrule{t-sub} that allows us to type $\mkkeyword{done}$ in any type
environment with irrelevant names.\Ugo{irrelevant types?}\Luca{\`E
  indifferente per la terminologia introdotta nella
  Definizione~\ref{def:classification}}

\DiscussRule{Message}
Rule \refrule{t-msg} establishes that a message
$\Sendu\Tag\seqof\NameV$ is well typed provided that the mailbox
$u$ allows the storing of an $\Tag$-tagged message with
arguments of type $\seqof\Type$ and the types of $\seqof\NameV$ are indeed
$\seqof\Type$.
The subsumption rule \refrule{t-sub} will make it possible to use
arguments whose type is a \emph{subtype} of the expected ones.
A message $\Sendu\Tag\seqof\NameV$ establishes dependencies between
the target mailbox $u$ and all of the arguments $\seqof\NameV$. We
write $\gedgeu{\set{v_1,\dots,v_n}}$ for the
dependency graph
$\gedgeu{v_1}\sqcup \cdots \sqcup
\gedgeu{v_n}$ and use $\emptyset$ for the empty graph union.

\DiscussRule{Process invocation}
The typing rule for a process invocation $\invoke\RecVar\seqof\NameU$
checks that there exists a global definition for $\RecVar$ which
expects exactly the given number and type of parameters. Again,
rule~\refrule{t-sub} will make it possible to use parameters whose
types are subtypes of the expected ones.
A process invocation yields the same dependencies as the
corresponding process definition, with the appropriate substitutions
applied.

\DiscussRule{Guards}
Guards are used to match the content of a mailbox and possibly
retrieve messages from it.
According to rule~\refrule{t-fail}, the action $\Failu$ matches
a mailbox $u$ with type $\ttqmark\mathbb{0}$, indicating that an
unexpected message has been found in the mailbox. The type
environment may contain arbitrary associations, since the
$\Failu$ action causes a runtime error.
Rule~\refrule{t-free} states that the action $\FreeuP$
matches a mailbox $u$ with type $\ttqmark\mathbb{1}$, indicating that the
mailbox is empty. The continuation is well typed in the residual
type environment $\Gamma$.
An input action $\Receiveu\Tag\seqof\VarXP$ matches a mailbox
$u$ with type $\ttqmark(\tmessage\Tag\seqof\Type \cdot E)$ that
guarantees the presence of an $\Tag$-tagged message possibly along
with other messages as specified by $E$. The continuation
$P$ must be well typed in an environment where the mailbox
has type $\ttqmarkE$, which describes the content of the mailbox
after the $\Tag$-tagged message has been removed. Associations for
the received arguments $\seqof\VarX$ are also added to the type
environment.
A compound guard $G_1 + G_2$ offers the actions
offered by $G_1$ and $G_2$ and therefore matches a mailbox
$u$ with type $\ttqmark(E_1 + E_2)$, where
$E_i$ is the pattern that describes the mailbox matched by
$G_i$. Note that the residual type environment $\Gamma$ is
the same in both branches, indicating that the type of other
mailboxes used by the guard cannot depend on that of $u$.

The judgments for guards do not yield any dependency graph. This is
compensated by the rule~\refrule{t-guard}, which we describe next.

\DiscussRule{Guarded processes}
Rule~\refrule{t-guard} is used to type a guarded process $G$,
which matches some mailbox $u$ of type $\ttqmarkE$ and
possibly retrieves messages from it.
As we have seen while discussing guards, $E$ is supposed to
be a pattern of the form $E_1 + \cdots + E_n$
where each $E_i$ is either $\mathbb{0}$, $\mathbb{1}$ or of the form
$\mathtt{M} \cdot F$. However, only the patterns
$E$ that are in \emph{normal form} are suitable to be used in
this typing rule and the side condition $\df{}E$ checks that
this is indeed the case. We motivate the need of a normal form by
means of a simple example.

Suppose that our aim is to type a process
$\Receiveu\Tag[A]{}P + \Receiveu\Tag[B]{}Q$
that consumes either an $\Tag[A]$ message or a $\Tag[B]$ message from
$u$, whichever of these two messages is matched first in
$u$, and then continues as $P$ or $Q$
correspondingly. Suppose also that the type of $u$ is
$\ttqmarkE$ with
$E \stackrel{\text{\tiny def}}= \Tag[A]\cdot\Tag[C] + \Tag[B]\cdot\Tag[A]$, which
allows the rules for guards to successfully type check the process.
As we have seen while discussing rule~\refrule{t-in}, $P$
and $Q$ must be typed in an environment where the type of
$u$ has been updated so as to reflect the fact that the consumed
message is no longer in the mailbox. In this particular case, we
might be tempted to infer that the type of $u$ in $P$ is
$\ttqmark\Tag[C]$ and that the type of $u$ in $Q$ is
$\ttqmark\Tag[A]$. Unfortunately, the type $\ttqmark\Tag[C]$ does not accurately
describe the content of the mailbox after $\Tag[A]$ has been consumed
because, according to $E$, the $\Tag[A]$ message may be
accompanied by \emph{either} a $\Tag[B]$ message \emph{or} by a
$\Tag[C]$ message, whereas $\ttqmark\Tag[C]$ only accounts for the second
possibility.
Thus, the appropriate pattern to be used for typing this process is
$\Tag[A] \cdot (\Tag[B] + \Tag[C]) + \Tag[B] \cdot \Tag[A]$, where the
fact that $\Tag[B]$ may be found after consuming $\Tag[A]$ is made
explicit.  This pattern and $E$ are equivalent as they
generate exactly the same set of valid configurations. Yet,
$\Tag[A] \cdot (\Tag[B] + \Tag[C]) + \Tag[B] \cdot \Tag[A]$ is in
normal form whereas $E$ is not.  In general the normal form
is not unique. For example, also the patterns
$\Tag[B] \cdot \Tag[A] + \Tag[C] \cdot \Tag[A]$ and
$\Tag[A] \cdot (\Tag[B] + \Tag[C])$ are in normal form and equivalent
to $E$ and can be used for typing processes that consume
messages from $u$ in different orders or with different
priorities.

The first ingredient for defining the notion of pattern normal form
is that of pattern residual $\pderE\mathtt{M}$, which
describes the content of a mailbox that initially contains a
configuration of messages described by $E$ and from which we
remove a single message with type $\mathtt{M}$:

\begin{definition}[pattern residual]
  \label{def:der}
  The \emph{residual} of a pattern $E$ with respect to an
  atom $\mathtt{M}$, written $\pderE\mathtt{M}$, is
  inductively defined by the following equations:
  \[
    \begin{array}{r@{~}c@{~}ll}
      \pder\mathbb{0}\mathtt{M} = \pder\mathbb{1}\mathtt{M} & \stackrel{\text{\tiny def}}= & \mathbb{0}
      \\
      \pder{(E^{\ast})}\mathtt{M} & \stackrel{\text{\tiny def}}= & \pderE\mathtt{M} \cdot E^{\ast}
    \end{array}
    ~
    \begin{array}{r@{~}c@{~}ll}
      \pder{\tmessage\Tag\seqof\TypeT}{\tmessage\Tag\seqof\TypeS} & \stackrel{\text{\tiny def}}= & \mathbb{1} & \text{if $\seqof\TypeT \leqslant \seqof\TypeS$}
      \\
      \pder{\tmessage\Tag\seqof\TypeT}{\tmessage{\Tag'}\seqof\TypeS} & \stackrel{\text{\tiny def}}= & \mathbb{0} & \text{if $\Tag \ne \Tag'$}
    \end{array}
    ~
    \begin{array}{r@{~}c@{~}ll}
      \pder{(E + F)}\mathtt{M} & \stackrel{\text{\tiny def}}= & \pderE\mathtt{M} + \pderF\mathtt{M}
      \\
      \pder{(E \cdot F)}\mathtt{M} & \stackrel{\text{\tiny def}}= & \pderE\mathtt{M} \cdot F + E \cdot \pderF\mathtt{M}
    \end{array}
  \]
\end{definition}

If we take the pattern $E$ discussed earlier we have
$\pderE\Tag[A] = \mathbb{1} \cdot \Tag[C] + \Tag[A] \cdot \mathbb{0}
+ \mathbb{0} \cdot \mathbb{1} + \Tag[B] \cdot \mathbb{1} \eqp \Tag[B] +
\Tag[C]$.
The pattern residual operator is closely related to Brzozowski's
derivative in a commutative Kleene
algebra~\cite{Brzozowski64,HopkinsKozen99}. Unlike Brzozowski's
derivative, the pattern residual is a partial operator:
$\pderE{\tmessage\Tag\seqof\TypeS}$ is defined provided that the
$\seqof\TypeS$ are supertypes of all types $\seqof\TypeT$ found in
$\Tag$-tagged atoms within $E$. This condition has a natural
justification: when choosing the message to remove from a mailbox
containing a configuration of messages described by $E$, only
the tag $\Tag$ of the message -- and not the type of its arguments
-- matters. Thus, $\seqof\TypeS$ faithfully describe the received
arguments provided that they are supertypes of \emph{all} argument
types of \emph{all} $\Tag$-tagged message types in $E$. For
example, assuming $\mkkeyword{nat} \leqslant \mkkeyword{int}$, we have that
$\pder{(\tmessage\Tag\mkkeyword{int} +
  \tmessage\Tag\mkkeyword{nat})}{\tmessage\Tag\mkkeyword{int}}$ is defined whereas
$\pder{(\tmessage\Tag\mkkeyword{int} +
  \tmessage\Tag\mkkeyword{nat})}{\tmessage\Tag\mkkeyword{nat}}$ is not.

We use the notion of pattern residual to define pattern normal
forms:

\begin{definition}[pattern normal form]
  \label{def:nf}
  We say that a pattern $E$ is in \emph{normal form}, written
  $\df{}E$, if $\dfE\Pattern$ is derivable by the
  following axioms and rules:
  \[
    \dfE\mathbb{0}
    \qquad
    \dfE\mathbb{1}
    \qquad
    \inferrule{
      F \eqp \pderE\mathtt{M}
    }{
      \dfE{\mathtt{M}\tmulF}
    }
    \qquad
    \inferrule{
      \df{E}{F_1}
      \\
      \df{E}{F_2}
    }{
      \dfE{F_1 + F_2}
    }
  \]
\end{definition}

Essentially, the judgment $\df{}E$ verifies that $E$
is expressed as a sum of $\mathbb{0}$, $\mathbb{1}$ and
$\mathtt{M}\tmulF$ terms where $F$ is (equivalent
to) the residual of $E$ with respect to $\mathtt{M}$.

A guarded process yields all the dependencies between the mailbox
$u$ being used and the names occurring free in the
continuations, because the process will not be able to exercise the
capabilities on these names until the message from $u$ has been
received.

\DiscussRule{Parallel composition}
Rule~\refrule{t-par} deals with parallel compositions of the form
$P_1 \mathbin\ttbar P_2$. This rule accounts for the fact that
the same mailbox $u$ may be used in both $P_1$ and
$P_2$ according to different types.  For example,
$P_1$ might store an $\Tag[A]$ message into $u$ and
$P_2$ might store a $\Tag[B]$ message into $u$. In the
type environment for the parallel composition as a whole we must be
able to express with a single type the combined usages of $u$ in
$P_1$ and $P_2$.  This is accomplished by introducing
an operator that combines types:

\begin{definition}[type combination]
  \label{def:type_combination}
  We write $\tau \mathbin{\|} \sigma$ for the \emph{combination} of
  $\tau$ and $\sigma$, where $\mathbin{\|}$ is the partial symmetric
  operator defined as follows:
  \[
    \ttemarkE \mathbin{\|} \ttemarkF \stackrel{\text{\tiny def}}= \ttemark\parens{E \cdot F}
    \qquad
    \ttemarkE \mathbin{\|} \ttqmark\parens{E \cdot F} \stackrel{\text{\tiny def}}= \ttqmarkF
    \qquad
    \ttqmark\parens{E \cdot F} \mathbin{\|} \ttemarkE \stackrel{\text{\tiny def}}= \ttqmarkF
  \]
\end{definition}

Continuing the previous example, we have
$\ttemark\Tag[A] \mathbin{\|} \ttemark\Tag[B] = \ttemark(\Tag[A] \cdot \Tag[B])$ because
storing one $\Tag[A]$ message and one $\Tag[B]$ message in $u$ means
storing an overall configuration of messages described by the
pattern $\Tag[A] \cdot \Tag[B]$.
When $u$ is used for both input and output operations, the
combined type of $u$ describes the overall balance of the
mailbox. For example, we have
$\ttemark\Tag[A] \mathbin{\|} \ttqmark(\Tag[A] \cdot \Tag[B]) = \ttqmark\Tag[B]$: if we combine a
process that stores an $\Tag[A]$ message into $u$ with another
process that consumes both an $\Tag[A]$ message and a $\Tag[B]$ message
from the same mailbox in some unspecified order, then we end up with
a process that consumes a $\Tag[B]$ message from $u$.

Notice that $\mathbin{\|}$ is a partial operator in that not all type
combinations are defined. It might be tempting to relax $\mathbin{\|}$ in
such a way that
$\ttemark(\Tag[A] \cdot \Tag[B]) \mathbin{\|} \ttqmark\Tag[A] = \ttemark\Tag[B]$, so as to
represent the fact that the combination of two processes results in
an excess of messages that must be consumed by some other process.
However, this would mean allowing different processes to consume
messages from the same mailbox, which is not safe in general (see
Example~\ref{ex:linear_input}).
For the same reason, the combination of $\ttqmarkE$ and
$\ttqmarkF$ is always undefined regardless of $E$ and
$F$.
Operators akin to $\mathbin{\|}$ for the combination of channel types are
commonly found in substructural type systems for the (linear)
$\pi$-calculus~\cite{SangiorgiWalker01,Padovani14B}. Unlike these
systems, in our case the combination concerns also the content of a
mailbox in addition to the capabilities for accessing it.

\begin{example}
  \label{ex:linear_input}
  Suppose that we extend the type combination operator so that
  $\ttqmark\parens{E \cdot F} = \ttqmarkE \mathbin{\|}
  \ttqmarkF$.  To see why this extension would be dangerous,
  consider the process
  \[
    \begin{array}{l}
      \bigparens{
        \Sendu\Tag[A]\mkconstant{True}
        \mathbin\ttbar
        \Receiveu\Tag[A]\Var[x]
        \parens{
          \Send\mathit{system}\Tag[print\ttunderscore bool]\Var[x]
          \mathbin\ttbar
          \Freeu
          \mkkeyword{done}
        }
      }
      \mathbin\ttbar
      {}
      \\
      \bigparens{
        \Sendu\Tag[A]{\mkint2}
        \mathbin\ttbar
        \Receiveu\Tag[A]\Var[y]
        \parens{
          \Send\mathit{system}\Tag[print\ttunderscore int]\Var[y]
          \mathbin\ttbar
          \Freeu
          \mkkeyword{done}
        }
      }
    \end{array}
  \]

  Overall, this process stores into $u$ a combination of
  messages that matches the pattern
  $\tmessage\Tag[A]\mkkeyword{bool} \cdot \tmessage\Tag[A]\mkkeyword{int}$ and retrieves
  from $u$ the same combination of messages. Apparently, $u$
  is used in a balanced way.
  %
  However, there is no guarantee that the $\Sendu\Tag[A]\mkconstant{True}$
  message is received by the process at the top and that the
  $\Sendu\Tag[A]{\mkint2}$ message is received by the process at
  the bottom. In fact, the converse may happen because only the tag
  of a message -- not the type or value of its arguments -- is used
  for matching messages in the mailbox calculus.
  %
  \hfill$\blacksquare$
\end{example}

We now extend type combination to type environments in the expected
way:

\begin{definition}[type environment combination]
  \label{def:cmul}
  We write $\Gamma \mathbin{\|} \Delta$ for the \emph{combination} of
  $\Gamma$ and $\Delta$, where $\mathbin{\|}$ is the partial operator
  inductively defined by the equations:
  \[
    \Gamma \mathbin{\|} \emptyset \stackrel{\text{\tiny def}}= \Gamma
    \qquad
    \emptyset \mathbin{\|} \Gamma \stackrel{\text{\tiny def}}= \Gamma
    \qquad
    (u : \tau, \Gamma) \mathbin{\|} (u : \sigma, \Delta) \stackrel{\text{\tiny def}}= u : \tau \mathbin{\|} \sigma, (\Gamma \mathbin{\|} \Delta)
  \]
\end{definition}

With this machinery in place, rule~\refrule{t-par} is
straightforward to understand and the dependency graph of
$P_1 \mathbin\ttbar P_2$ is simply the union of the dependency
graphs of $P_1$ and $P_2$.

\DiscussRule{Mailbox restriction}
Rule~\refrule{t-new} establishes that the process creating a new
mailbox $a$ with scope $P$ is well typed provided that
the type of $a$ is $\ttqmark\mathbb{1}$. This means that every message
stored in the mailbox $a$ by (a sub-process of) $P$ is
also consumed by (a sub-process of) $P$.
The dependency graph of the process is the same as that of
$P$, except that $a$ is restricted.

\DiscussRule{Subsumption}
As we have anticipated earlier in a few occasions, the subsumption
rule \refrule{t-sub} allows us to rewrite types in the type
environment and to introduce associations for irrelevant names.  The
rule makes use of the following notion of subtyping for type
environments:

\begin{definition}[subtyping for type environments]
  We say that $\Gamma$ is a \emph{subtype environment} of
  $\Delta$ if $\Gamma \leqslant \Delta$, where $\leqslant$ is the
  least preorder on type environments such that:
  \[
    \inferrule{
      \mathstrut
    }{
      u : \ttemark\mathbb{1}, \Gamma \leqslant \Gamma
    }
    \qquad
    \inferrule{
      \tau \leqslant \sigma
    }{
      u : \tau, \Gamma \leqslant u : \sigma, \Gamma
    }
  \]
\end{definition}

Intuitively, $\Gamma \leqslant \Delta$ means that $\Gamma$
provides more capabilities than $\Delta$. For example,
$u : \ttemark(\Tag[A] + \Tag[B]), v : \ttemark\mathbb{1} \leqslant
u : \ttemark\Tag[A]$ since a process that is well typed in the
environment $u : \ttemark\Tag[A]$ stores an $\Tag[A]$ message into
$u$, which is also a valid behavior in the environment
$u : \ttemark(\Tag[A] + \Tag[B]), v : \ttemark\mathbb{1}$ where
$u$ has more capabilities (it is also possible to store a
$\Tag[B]$ message into $u$) and there is an irrelevant name
$v$ not used by the process.

{ Rule~\refrule{t-sub} also allows us to replace the
  dependency graph yielded by $P$ with another one that
  generates a superset of dependencies. In general, the dependency
  graph should be kept as small as possible to minimize the
  possibility of yielding mutual dependencies (see
  \refrule{t-par}). The replacement allowed by \refrule{t-sub} is
  handy for technical reasons, but not necessary. The point is that
  the residual of a process typically yields fewer dependencies than
  the process itself, so we use \refrule{t-sub} to enforce the
  invariance of dependency graphs across reductions.  }

\begin{example}
  \label{ex:lock_derivation}
  We show the full typing derivation for $\RecVar[FreeLock]$ and
  $\RecVar[BusyLock]$ defined in Example~\ref{ex:lock}.  Our objective is
  to show the consistency of the global process declarations
  \[
    \RecVar[FreeLock] : (\Var[self] : \tau; \emptyset)
    \qquad
    \RecVar[BusyLock] : (\Var[self] : \tau, \Var[owner] : \rho; \gedge\Var[self]\Var[owner])
  \]
  where $\tau \stackrel{\text{\tiny def}}= \ttqmark\tmessage\Tag[acquire]\rho^{\ast}$ and
  $\rho \stackrel{\text{\tiny def}}= \ttemark{\tmessage\Tag[reply]{\ttemark\Tag[release]}}$.  In the
  derivation trees below we rename $\Var[self]$ as $\Var[x]$ and
  $\Var[owner]$ and $\Var[y]$ to resonably fit the derivations within
  the page limits. We start from the body of $\RecVar[BusyLock]$, which
  is simpler, and obtain
  \[
    \begin{prooftree}
      \[
        \justifies
        \wtp{
          \Var[x] : \ttemark\Tag[release],
          \Var[y] : \rho
        }{
          \Send\Var[y]\Tag[reply]\Var[x]
        }{
          \gedge\Var[y]\Var[x]
        }
        \using\refrule{t-msg}
      \]
      \[
        \[
          \[
            \justifies
            \wtp{
              \Var[x] : \tau
            }{
              \invoke\RecVar[FreeLock]\Var[x]
            }{
              \emptyset
            }
            \using\refrule{t-def}
          \]
          \justifies
          \wtg{
            \Var[x] : \sigma
          }{
            \Receive\Var[x]\Tag[release]{}
            \invoke\RecVar[FreeLock]\Var[x]
          }
          \using\refrule{t-in}
        \]
        \justifies
        \wtp{
          \Var[x] : \sigma
        }{
          \Receive\Var[x]\Tag[release]{}
          \invoke\RecVar[FreeLock]\Var[x]
        }{
          \emptyset
        }
        \using\refrule{t-guard}
      \]
      \justifies
      \wtp{
        \Var[x] : \tau, \Var[y] : \rho
      }{
        \Send\Var[y]\Tag[reply]\Var[x]
        \mathbin\ttbar
        \Receive\Var[x]\Tag[release]{}
        \invoke\RecVar[Lock]\Var[x]
      }{
        \gedge\Var[y]\Var[x] \sqcup \emptyset
      }
      \using\refrule{t-par}
    \end{prooftree}
  \]
  where
  $\sigma \stackrel{\text{\tiny def}}= \ttqmark{(\Tag[release] \cdot
    \tmessage\Tag[acquire]\rho^{\ast})}$.

  Concerning $\RecVar[FreeLock]$, the key step is rewriting the pattern
  of $\tau$ in a normal form that matches the branching structure
  of the process. To this aim, we use the property
  $E^{\ast} \eqp \mathbb{1} + E \cdot E^{\ast}$
  and the fact that $\mathbb{0}$ is absorbing for the product
  connective:
  \[
    \begin{prooftree}
      \[
        \[
          \qquad\qquad
          \vdots
          \qquad\qquad
          \[
            \[
              \[
                \justifies
                \wtg{
                  \Var[x] : \ttqmark\mathbb{0}
                }{
                  \Fail\Var[x]
                }
                \using\refrule{t-fail}
              \]
              \justifies
              \wtp{
                \Var[x] : \ttqmark\mathbb{0}
              }{
                \Fail\Var[x]
              }{
                \emptyset
              }
              \using\refrule{t-guard}
            \]
            \using\refrule{t-guard}
            \justifies
            \wtg{
              \Var[x] : \ttqmark(\Tag[release]\cdot\mathbb{0})
            }{
              \Receive\Var[x]\Tag[release]{}
              \Fail\Var[x]
            }
            \using\refrule{t-in}
          \]
          \justifies
          \wtg{
            \Var[x] :
            \ttqmark\parens{
              \mathbb{1}
              +
              \tmessage\Tag[acquire]\rho \cdot \tmessage\Tag[acquire]\rho^{\ast}
              +
              \Tag[release] \cdot \mathbb{0}
            }
          }{
            {}
            \cdots
            +
            \Receive\Var[x]\Tag[release]{}
            \Fail\Var[x]
          }
          \using\refrule{t-branch}
        \]
        \justifies
        \wtp{
          \Var[x] :
          \ttqmark\parens{
            \mathbb{1}
            +
            \tmessage\Tag[acquire]\rho \cdot \tmessage\Tag[acquire]\rho^{\ast}
            +
            \Tag[release] \cdot \mathbb{0}
          }
        }{
          {}
          \cdots
          +
          \Receive\Var[x]\Tag[release]{}
          \Fail\Var[x]
        }{
          \emptyset
        }
        \using\refrule{t-guard}
      \]
      \justifies
      \wtp{
        \Var[x] : \tau
      }{
        \Free\Var[x]\mkkeyword{done}
        +
        \cdots
        +
        \Receive\Var[x]\Tag[release]{}
        \Fail\Var[x]
      }{
        \emptyset
      }
      \using\refrule{t-sub}
    \end{prooftree}
  \]

  The elided sub-derivation concerns the first two branches of
  $\RecVar[FreeLock]$ and is as follows:
  \[
    \begin{prooftree}
      \[
        \[
          \justifies
          \wtp{
            \emptyset
          }{
            \mkkeyword{done}
          }{
            \emptyset
          }
          \using\refrule{t-done}
        \]
        \justifies
        \wtg{
          \Var[x] : \ttqmark\mathbb{1}
        }{
          \Free\Var[x]\mkkeyword{done}
        }
        \using\refrule{t-free}
      \]
      \[
        \[
          \justifies
          \wtp{
            \Var[x] : \tau,
            \Var[y] : \rho
          }{
            \invoke\RecVar[BusyLock]{\Var[x],\Var[y]}
          }{
            \gedge\Var[x]\Var[y]
          }
          \using\refrule{t-def}
        \]
        \justifies
        \wtg{
          \Var[x] :
          \ttqmark\tmessage\Tag[acquire]\rho \cdot \tmessage\Tag[acquire]\rho^{\ast}
        }{
          \Receive\Var[x]\Tag[acquire]\Var[y]
          \invoke\RecVar[BusyLock]{\Var[x],\Var[y]}
        }
        \using\refrule{t-in}
      \]
      \justifies
      \wtg{
        \Var[x] :
        \ttqmark\parens{
          \mathbb{1}
          +
          \tmessage\Tag[acquire]\rho \cdot \tmessage\Tag[acquire]\rho^{\ast}
        }
      }{
        \Free\Var[x]\mkkeyword{done}
        +
        \Receive\Var[x]\Tag[acquire]\Var[y]
        \invoke\RecVar[BusyLock]{\Var[x],\Var[y]}
      }
      \using\refrule{t-branch}
    \end{prooftree}
  \]

  The process~\eqref{eq:alice_carol}, combining an instance of the
  lock and the users $\Var[alice]$ and $\Var[carol]$, is also well
  typed. As we will see at the end of Section~\ref{sec:properties},
  this implies that both $\Var[alice]$ and $\Var[carol]$ are able to
  acquire the lock, albeit in some unspecified order.
  %
  \hfill$\blacksquare$
\end{example}

\begin{example}
  \label{ex:future_deadlock}
  In this example we show that the
  process~\eqref{eq:future_deadlock} of Example~\ref{ex:future} is
  ill typed. In order to do so, we assume the global process
  declaration
  \[
    \RecVar[Future] : (\Var[self] : \ttqmark(\tmessage\Tag[put]\mkkeyword{int} \cdot
    \tmessage\Tag[get]{\ttemark\tmessage\Tag[reply]\mkkeyword{int}}^{\ast}); \emptyset)
  \]
  which can be shown to be consistent with the given definition for
  $\RecVar[Future]$.
  %
  In the derivation below we use the pattern
  $F \stackrel{\text{\tiny def}}= \tmessage\Tag[put]\mkkeyword{int} \cdot
  \tmessage\Tag[get]\rho^{\ast}$ and the types
  $\tau \stackrel{\text{\tiny def}}= \ttemark\tmessage\Tag[put]\mkkeyword{int}$,
  $\sigma \stackrel{\text{\tiny def}}= \ttqmark\parens{\tmessage\Tag[reply]\mkkeyword{int} \cdot \mathbb{1}}$
  and $\rho \stackrel{\text{\tiny def}}= \ttemark\tmessage\Tag[reply]\mkkeyword{int}$:
  \[
    \begin{prooftree}
      \[
        \[
          \[
            \justifies
            \wtp{
              \Var[f] : \ttemark\tmessage\Tag[get]\rho,
              c : \rho
            }{
              \Send\Var[f]\TagGetc
            }{
              \gedge\VarFuturec
            }
            \using\refrule{t-msg}
          \]
          \[
            \[
              \[
                \[
                  \[
                    \justifies
                    \wtp{
                      \Var[f] : \tau, \Var : \mkkeyword{int}
                    }{
                      \Send\Var[f]\Tag[put]\Var
                    }{
                      \emptyset
                    }
                    \using\refrule{t-msg}
                  \]
                  \justifies
                  \wtg{
                    \Var[f] : \tau, c : \ttqmark\mathbb{1}, \Var : \mkkeyword{int}
                  }{
                    \Freec
                    \Send\Var[f]\Tag[put]\Var
                  }
                  \using\refrule{t-free}
                \]
                \justifies
                \wtp{
                  \Var[f] : \tau, c : \ttqmark\mathbb{1}, \Var : \mkkeyword{int}
                }{
                  \Freec
                  \Send\Var[f]\Tag[put]\Var
                }{
                  \gedgec\Var[f]
                }
                \using\refrule{t-guard}
              \]
              \justifies
              \wtg{
                \Var[f] : \tau, c : \sigma
              }{
                \Receivec\Tag[reply]\Var
                \Freec
                \Send\Var[f]\Tag[put]\Var
              }
              \using\refrule{t-in}
            \]
            \justifies
            \wtp{
              \Var[f] : \tau, c : \sigma
            }{
              \Receivec\Tag[reply]\Var
              \Freec
              \Send\Var[f]\Tag[put]\Var
            }{
              \gedgec\Var[f]
            }
            \using\refrule{t-guard}
          \]
          \justifies
          \wtp{
            \Var[f] : \ttemark\parens{
              \tmessage\Tag[get]\rho
              \cdot
              \tmessage\Tag[put]\mkkeyword{int}
            },
            c : \ttqmark\mathbb{1}
          }{
            \Send\Var[f]\TagGetc
            \mathbin\ttbar
            \Receivec\Tag[reply]\Var
            \Freec
            \Send\Var[f]\Tag[put]\Var
          }{
            {-}
          }
          \using\refrule{t-par}
        \]
        \justifies
        \wtp{
          \Var[f] : \ttemarkF,
          c : \ttqmark\mathbb{1}
        }{
          \Send\Var[f]\TagGetc
          \mathbin\ttbar
          \Receivec\Tag[reply]\Var
          \Freec
          \Send\Var[f]\Tag[put]\Var
        }{
          {-}
        }
        \using\refrule{t-sub}
      \]
      \justifies
      \wtp{
        \Var[f] : \ttemarkF
      }{
        \Newc\parens{
          \Send\Var[f]\TagGetc
          \mathbin\ttbar
          \Receivec\Tag[reply]\Var
          \Freec
          \Send\Var[f]\Tag[put]\Var
        }
      }{
        {-}
      }
      \using\refrule{t-new}
    \end{prooftree}
  \]

  In attempting this derivation we have implicitly extended the
  typing rules so that names with type $\mkkeyword{int}$ do not contribute in
  generating any significant dependency. The critical point of the
  derivation is the application of \refrule{t-par}, where we are
  composing two parallel processes that yield a circular dependency
  between $c$ and $\Var[f]$. In the process on the left
  hand side, the dependency $\gedge\VarFuturec$ arises
  because $c$ is sent as a reference in a message targeted
  to $\Var[f]$. In the process on the right hand side, the
  dependency $\gedgec\Var[f]$ arises because there are
  guards concerning the mailbox $c$ that block an output
  operation on the mailbox $\Var[f]$.
  %
  \hfill$\blacksquare$
\end{example}

\begin{example}[non-deterministic choice]
  \label{ex:choice}
  Different input actions in the same guard can match messages with
  the same tag. This feature can be used to encode in the mailbox
  calculus the non-deterministic choice between $P_1$ and
  $P_2$ as the process
  \begin{equation}
    \label{eq:choice}
    \Newa\parens{
      \Senda\Tag{}
      \mathbin\ttbar
      \Receivea\Tag{}
      \Freea
      P_1
      +
      \Receivea\Tag{}
      \Freea
      P_2
    }
  \end{equation}
  provided that $\wtp\Gamma{P_i}{\varphi_i}$ for $i=1,2$.
  That is, $P_1$ and $P_2$ must be well typed in the
  same type environment. Below is the typing derivation for
  \eqref{eq:choice}
  \[
    \begin{prooftree}
      \[
        \[
          \justifies
          \wtp{
            a : \ttemark\Tag
          }{
            \Senda\Tag{}
          }{
            \emptyset
          }
          \using\refrule{t-msg}
        \]
        \[
          \[
            \[
              \[
                \[
                  \[
                    \wtp\Gamma{
                      P_i
                    }{
                      \varphi_i
                    }
                    \justifies
                    \wtg{
                      \Gamma, a : \ttqmark\mathbb{1}
                    }{
                      \Freea
                      P_i
                    }
                    \using\refrule{t-free}
                  \]
                  \justifies
                  \wtp{
                    \Gamma, a : \ttqmark\mathbb{1}
                  }{
                    \Freea
                    P_i
                  }{
                    \varphi
                  }
                  \using\refrule{t-guard}
                \]
                \justifies
                \wtg{
                  \Gamma, a : \ttqmark(\Tag \cdot \mathbb{1})
                }{
                  \Receivea\Tag{}
                  \Freea
                  P_i
                }
                \using\refrule{t-in}, i=1,2
              \]
              \justifies
              \wtg{
                \Gamma, a : \ttqmark(\Tag \cdot \mathbb{1} + \Tag \cdot \mathbb{1})
              }{
                \Receivea\Tag{}
                \Freea
                P_1
                +
                \Receivea\Tag{}
                \Freea
                P_2
              }
              \using\refrule{t-branch}
            \]
            \justifies
            \wtp{
              \Gamma, a : \ttqmark(\Tag \cdot \mathbb{1} + \Tag \cdot \mathbb{1})
            }{
              \Receivea\Tag{}
              \Freea
              P_1
              +
              \Receivea\Tag{}
              \Freea
              P_2
            }{
              \varphi
            }
            \using\refrule{t-guard}
          \]
          \justifies
          \wtp{
            \Gamma, a : \ttqmark(\Tag \cdot \mathbb{1})
          }{
            \Receivea\Tag{}
            \Freea
            P_1
            +
            \Receivea\Tag{}
            \Freea
            P_2
          }{
            \varphi
          }
          \using\refrule{t-sub}
        \]
        \justifies
        \wtp{
          \Gamma, a : \ttqmark\mathbb{1}
        }{
          \Senda\Tag{}
          \mathbin\ttbar
          \Receivea\Tag{}
          \Freea
          P_1
          +
          \Receivea\Tag{}
          \Freea
          P_2
        }{
          \varphi
        }
        \using\refrule{t-par}
      \]
      \justifies
      \wtp\Gamma{
        \Newa\parens{
          \Senda\Tag{}
          \mathbin\ttbar
          \Receivea\Tag{}
          \Freea
          P_1
          +
          \Receivea\Tag{}
          \Freea
          P_2
        }
      }{
        \Newa\varphi
      }
      \using\refrule{t-new}
    \end{prooftree}
  \]
  where $\varphi \stackrel{\text{\tiny def}}= \gedgea{\mathsf{dom}(\Gamma)}$.  The key
  step is the application of \refrule{t-sub}, which exploits the
  idempotency of $+$ (in patterns) to rewrite $\Tag \cdot \mathbb{1}$
  as the equivalent pattern
  $\Tag \cdot \mathbb{1} + \Tag \cdot \mathbb{1}$.
  %
  \hfill$\blacksquare$
\end{example}

\subsection{Mailbox Types}
\label{sec:types}

\begin{table}
  \begin{center}
    \[
      \begin{array}{rrcll}
        \textbf{Type} & \tau, \sigma
        & ::= & \ttqmarkE & \text{(input)}
        \\
        & & | & \ttemarkE & \text{(output)}
        \\\\
        \textbf{Pattern} & E, F
        & ::= & \mathbb{0} & \text{(unreliable mailbox)}
        \\
        & & | & \mathbb{1} & \text{(empty mailbox)}
        \\
        & & | & \tmessage\Tag\seqof\Type & \text{(atom)}
        \\
        & & | & E + F & \text{(sum)}
        \\
        & & | & E \cdot F & \text{(product)}
        \\
        & & | & E^{\ast} & \text{(exponential)}
      \end{array}
    \]
  \end{center}
  \caption{\label{tab:types} Syntax of mailbox types and patterns.}
\end{table}

The syntax of mailbox types and patterns is shown in
Table~\ref{tab:types}.
Patterns are \emph{commutative regular expressions}~\cite{Conway71}
describing the configurations of messages stored in a mailbox.
An atom $\tmessage\Tag\seqof\Type$ describes a mailbox containing a
single message with tag $\Tag$ and arguments of type $\seqof\Type$. We
let $\mathtt{M}$ range over atoms and abbreviate
$\tmessage\Tag\seqof\Type$ with $\Tag$ when $\seqof\Type$ is the empty
sequence.
Compound patterns are built using sum ($E + F$),
product ($E \cdot F$) and exponential
($E^{\ast}$).
The constants $\mathbb{1}$ and $\mathbb{0}$ respectively describe the empty
and the unreliable mailbox. There is no configuration of messages
stored in an unreliable mailbox, not even the empty one. We will use
the $\mathbb{0}$ pattern for describing mailboxes from which an
unexpected message has been received.
Let us look at a few simple examples.
The pattern $\Tag[A] + \Tag[B]$ describes a mailbox that contains
either an $\Tag[A]$ message or a $\Tag[B]$ message, but not both,
whereas the pattern $\Tag[A] + \mathbb{1}$ describes a mailbox that
either contains a $\Tag[A]$ message or is empty.
The pattern $\Tag[A] \cdot \Tag[B]$ describes a mailbox that contains
both an $\Tag[A]$ message and also a $\Tag[B]$ message. Note that
$\Tag[A]$ and $\Tag[B]$ may be equal, in which case the mailbox contains
\emph{two} $\Tag[A]$ messages.
Finally, the pattern $\Tag[A]^{\ast}$ describes a mailbox that contains
an arbitrary number (possibly zero) of $\Tag[A]$ messages.

A \emph{mailbox type} consists of a \emph{capability} (either $\ttqmark$
or $\ttemark$) paired with a pattern. The capability specifies whether
the pattern describes messages to be received from ($\ttqmark$) or stored
in ($\ttemark$) the mailbox. Here are some examples:
A process using a mailbox of type $\ttemark\Tag[A]$ \emph{must} store an
$\Tag[A]$ message into the mailbox, whereas a process using a mailbox
of type $\ttqmark\Tag[A]$ is guaranteed to receive an $\Tag[A]$ message from
the mailbox.
A process using a mailbox of type $\ttemark(\Tag[A] + \mathbb{1})$
\emph{may} store an $\Tag[A]$ message into the mailbox, but is not
obliged to do so.
A process using a mailbox of type $\ttemark\parens{\Tag[A] + \Tag[B]}$
decides whether to store an $\Tag[A]$ message or a $\Tag[B]$ message in
the mailbox, whereas a process using a mailbox of type
$\ttqmark\parens{\Tag[A] + \Tag[B]}$ must be ready to receive both kinds
of messages.
A process using a mailbox of type $\ttqmark\parens{\Tag[A] \cdot \Tag[B]}$ is
guaranteed to receive both an $\Tag[A]$ message and a $\Tag[B]$ message
and may decide in which order to do so. A process using a mailbox of
type $\ttemark\parens{\Tag[A] \cdot \Tag[B]}$ must store both $\Tag[A]$ and
$\Tag[B]$ into the mailbox.
A process using a mailbox of type $\ttemark{\Tag[A]^{\ast}}$ decides how
many $\Tag[A]$ messages to store in the mailbox, whereas a process
using a mailbox of type $\ttqmark{\Tag[A]^{\ast}}$ must be prepared to
receive an arbitrary number of $\Tag[A]$ messages.

To cope with possibly infinite types we interpret the productions in
Table~\ref{tab:types} coinductively and consider as types the
regular trees~\cite{Courcelle83} built using those productions. We
require every infinite branch of a type tree to go through
infinitely many atoms. This strengthened contractiveness condition
allows us to define functions inductively on the structure of
patterns, provided that these functions do not recur into argument
types (\emph{cf.}\xspace Definitions~\ref{def:subp} and~\ref{def:der}).

The semantics of patterns is given in terms of sets of multisets of
atoms. Because patterns include types, the given semantics is
parametric in the subtyping relation, which will be defined next:

\begin{definition}[subpattern]
  \label{def:subp}
  The \emph{configurations} of $E$ are inductively defined by
  the following equations, where $\mathsf{A}$ and $\mathsf{B}$ range over
  multisets $\bag{\seqof\mathtt{M}}$ of atoms and $\uplus$
  denotes multiset union:
  \[
    \begin{array}[c]{@{}r@{~}c@{~}l@{}}
      \sem\mathbb{0} & \stackrel{\text{\tiny def}}= & \emptyset
      \\
      \sem\mathbb{1} & \stackrel{\text{\tiny def}}= & \set{\bag{}}
    \end{array}
    \qquad
    \begin{array}[c]{@{}r@{~}c@{~}l@{}}
      \sem{E + F} & \stackrel{\text{\tiny def}}= & \semE \cup \semF
      \\
      \sem{E \cdot F} & \stackrel{\text{\tiny def}}= & \set{ \mathsf{A} \uplus \mathsf{B} \mid \mathsf{A} \in \semE, \mathsf{B} \in \semF }
    \end{array}
    \qquad
    \begin{array}[c]{@{}r@{~}c@{~}l@{}}
      \sem\mathtt{M} & \stackrel{\text{\tiny def}}= & \set{\bag\mathtt{M}}
      \\
      \sem{E^{\ast}} & \stackrel{\text{\tiny def}}= & \sem\mathbb{1} \cup \semE \cup
      \sem{E\tmulE} \cup \cdots
    \end{array}
  \]

  Given a preorder relation $\mathrel{\mathcal{R}}$ on types, we write
  $E \subp[\mathrel{\mathcal{R}}] F$ if
  $\bag[i\in I]{\tmessage{\Tag_i}{\seqof\TypeT_i}} \in \semE$
  implies
  $\bag[i\in I]{\tmessage{\Tag_i}{\seqof\TypeS_i}} \in \semF$ and
  $\seqof\TypeT_i \mathrel{\mathcal{R}} \seqof\TypeS_i$ for every $i\in I$.
  %
  We write $\eqp[\mathrel{\mathcal{R}}]$ for ${\subp[\mathrel{\mathcal{R}}]} \cap {\supp[\mathrel{\mathcal{R}}]}$.
\end{definition}

For example,
$\sem{\Tag[A] + \Tag[B]} = \set{ \bag\Tag[A], \bag\Tag[B] }$ and
$\sem{\Tag[A] \cdot \Tag[B]} = \set{ \bag{\Tag[A], \Tag[B]} }$.
It is easy to see that $\subp[\mathrel{\mathcal{R}}]$ is a pre-congruence with
respect to all the connectives and that it includes all the known
laws of commutative Kleene algebra~\cite{Conway71}: both $+$ and
$\cdot$ are commutative and associative, $+$ is idempotent and
has unit $\mathbb{0}$, $\cdot$ distributes over $+$, it has unit
$\mathbb{1}$ and is absorbed by $\mathbb{0}$.  Also observe that
$\subp[\mathrel{\mathcal{R}}]$ is related covariantly to $\mathrel{\mathcal{R}}$, that is
$\seqof\TypeT \mathrel{\mathcal{R}} \seqof\TypeS$ implies
$\tmessage\Tag\seqof\TypeT \subp[\mathrel{\mathcal{R}}]
\tmessage\Tag\seqof\TypeS$.

We now define subtyping. As types may be infinite, we resort to
coinduction:

\begin{definition}[subtyping]
  \label{def:subt}
  We say that $\mathrel{\mathcal{R}}$ is a \emph{subtyping relation} if
  $\tau \mathrel{\mathcal{R}} \sigma$ implies either
  \begin{enumerate}
  \item\label{subt:input} $\tau = \ttqmarkE$ and
    $\sigma = \ttqmarkF$ and $E \subp[\mathrel{\mathcal{R}}] F$,
    or
  \item\label{subt:output} $\tau = \ttemarkE$ and
    $\sigma = \ttemarkF$ and $F \subp[\mathrel{\mathcal{R}}] E$.
  \end{enumerate}
  %
  We write $\leqslant$ for the largest subtyping relation and say that
  $\tau$ is a \emph{subtype} of $\sigma$ (and $\sigma$ a
  \emph{supertype} of $\tau$) if $\tau \leqslant \sigma$.
  %
  We write $\lessgtr$ for ${\leqslant} \cap {\geqslant}$, $\subp$ for
  $\subp[\leqslant]$ and $\eqp$ for $\eqp[\leqslant]$.
\end{definition}

Items~\ref{subt:input} and~\ref{subt:output} respectively correspond
to the usual covariant and contravariant rules for channel types
with input and output capabilities~\cite{PierceSangiorgi96}.  For
example, $\ttemark\parens{\Tag[A] + \Tag[B]} \leqslant \ttemark\Tag[A]$ because a
mailbox of type $\ttemark\parens{\Tag[A] + \Tag[B]}$ is more permissive
than a mailbox of type $\ttemark\Tag[A]$. Dually,
$\ttqmark\Tag[A] \leqslant \ttqmark\parens{\Tag[A] + \Tag[B]}$ because a mailbox of
type $\ttqmark\Tag[A]$ provides stronger guarantees than a mailbox of type
$\ttqmark\parens{\Tag[A] + \Tag[B]}$.
Note that
$\ttemark\parens{\Tag[A] \cdot \Tag[B]} \lessgtr \ttemark\parens{\Tag[B] \cdot \Tag[A]}$
and
$\ttqmark\parens{\Tag[A] \cdot \Tag[B]} \lessgtr \ttqmark\parens{\Tag[B] \cdot \Tag[A]}$,
to witness the fact that the order in which messages are stored in a
mailbox is irrelevant.

Mailbox types whose patterns are in particular relations with the
constants $\mathbb{0}$ and $\mathbb{1}$ will play special roles, so we
introduce some corresponding terminology.

\begin{definition}[type and name classification]
  \label{def:classification}
  We say that (a name whose type is) $\tau$ is:
  \begin{itemize}
  \item \emph{relevant} if $\tau \not\leqslant \ttemark\mathbb{1}$ and
    \emph{irrelevant} otherwise;
  \item \emph{reliable} if $\tau \not\leqslant \ttqmark\mathbb{0}$ and
    \emph{unreliable} otherwise;
  \item \emph{usable} if $\ttemark\mathbb{0} \not\leqslant \tau$ and
    \emph{unusable} otherwise.
  \end{itemize}
\end{definition}

A relevant name \emph{must} be used, whereas an irrelevant name may
be discarded because not storing any message in the mailbox it
refers to is allowed by its type. All mailbox types with input
capability are relevant.
A reliable mailbox is one from which no unexpected message has been
received. All names with output capability are reliable.
A usable name \emph{can} be used, in the sense that there exists a
construct of the mailbox calculus that expects a name with that
type. All mailbox types with input capability are usable, but
$\ttqmark(\Tag[A] \cdot \mathbb{0})$ is unreliable.
Both $\ttemark\Tag[A]$ and $\ttemark\parens{\mathbb{1} + \Tag[A]}$ are
usable. The former type is also relevant because a process using a
mailbox with this type must (eventually) store an $\Tag[A]$ message
in it. On the contrary, the latter type is irrelevant, since not
using the mailbox is a legal way of using it.

\begin{center}
  \fbox{
    \parbox{0.95\textwidth}{%

      \textit{Henceforth we assume that all types are usable and
        that all argument types are also reliable. That is, we ban
        all types like $\ttemark\mathbb{0}$ or $\ttemark(\mathbb{0}\cdot\Tag)$ and
        all types like $\ttqmark\tmessage\Tag{\ttqmark\mathbb{0}}$ or
        $\ttemark\tmessage\Tag{\ttqmark\mathbb{0}}$.
        Example~\ref{ex:global_assumptions} in
        Appendix~\ref{sec:prop_subtyping} discusses the technical
        motivation for these assumptions.}

    }
  }
\end{center}

\begin{example}[lock type]
  \label{ex:lock_type}
  The mailbox used by the lock (Example~\ref{ex:lock}) will have
  several different types, depending on the viewpoint we take
  (either the lock itself or one of its users) and on the state of
  the lock (whether it is free or busy).
  %
  As we can see from the definition of $\RecVar[FreeLock]$, a free lock
  waits for an $\Tag[acquire]$ message which is supposed to carry a
  reference to another mailbox into which the capability to release
  the lock is stored. Since the lock is meant to have several
  concurrent users, it is not possible in general to predict the
  number of $\Tag[acquire]$ messages in its mailbox.  Therefore, the
  mailbox of a free lock has type
  \[
    \ttqmark\tmessage\Tag[acquire]{\ttemark\tmessage\Tag[reply]{\ttemark\Tag[release]}}^{\ast}
  \]
  from the viewpoint of the lock itself. When the lock is busy, it
  expects to find one $\Tag[release]$ message in its mailbox, but in
  general the mailbox will also contain $\Tag[acquire]$ messages
  corresponding to pending acquisition requests. So, the mailbox of
  a busy lock has type
  \[
    \ttqmark\parens{\Tag[release]\cdot\tmessage\Tag[acquire]{\ttemark\tmessage\Tag[reply]{\ttemark\Tag[release]}}^{\ast}}
  \]
  indicating that the mailbox contains (or will eventually contain)
  a single $\Tag[release]$ message along with arbitrarily many
  $\Tag[acquire]$ messages.

  Prospective owners of the lock may have references to the lock's
  mailbox with type
  $\ttemark\tmessage\Tag[acquire]{\ttemark\tmessage\Tag[reply]{\ttemark\Tag[release]}}$
  or
  $\ttemark\tmessage\Tag[acquire]{\ttemark\tmessage\Tag[reply]{\ttemark\Tag[release]}}^{\ast}$
  depending on whether they acquire the lock exactly once (just like
  $\Var[alice]$ and $\Var[carol]$ in Example~\ref{ex:lock}) or several
  times. Other intermediate types are possible in the case of users
  that acquire the lock a bounded number of times.
  %
  The current owner of the lock will have a reference to the lock's
  mailbox of type $\ttemark\Tag[release]$. This type is relevant, implying
  that the owner must eventually release the lock.
  %
  \hfill$\blacksquare$
\end{example}

\section{A Mailbox Type System}
\label{sec:type_system}

In this section we detail the type system for the mailbox
calculus. We start from the syntax and semantics of mailbox types
(Section~\ref{sec:types}) and of dependency graphs
(Section~\ref{sec:graphs}), the mechanism we use to track mailbox
dependencies. Then we present the typing rules
(Section~\ref{sec:rules}) and the properties of well-typed processes
(Section~\ref{sec:properties}).

\input{types}
\input{graphs}
\input{rules}
\input{properties}

redpajama_set_name: RedPajamaArXiv