Causally Consistent Reversible Choreographies\thanks{Revision of May 25, 2017. This work was partially supported by COST Actions IC1201 (Behavioral Types for Reliable Large-Scale Software Systems), IC1402 (Runtime Verification beyond Monitoring), and IC1405 (Reversible Computation - Extending Horizons of Computing). P\'{e
Claudio Antares Mezzina
IMT School for Advanced Studies Lucca
Italy
Jorge A. P\'{e
%Reversible programming models are foundational models of fault-tolerant, distributed communication. Under a reversible semantics, computation steps can be undone. % as a response to unanticipated events. This paper addresses the integration of reversible semantics into process languages for communication-centric systems, equipped with behavioral types. %This integration must reconcile the memories that support %reversible actions and monitors, the run-time entities that govern communication protocols. In prior work, we introduced a monitors-as-memories approach to seamlessly integrate reversible semantics into a process model in which concurrency is governed by session types (a class of behavioral types), covering binary (two-party) protocols with syn\-chro\-nous communications. Although such a model offers a simple setting for showcasing our approach, its expressiveness is rather limited. Here we substantially extend our approach, and use it to define reversible semantics for a very expressive process model that accounts for multiparty ($n$-party) protocols (choreographies), asynchronous communication, decoupled rollbacks, and process passing. As main technical result, we prove that our multiparty, reversible semantics is causally-consistent.
appendix.tex
% !TEX root = revchor.tex

%\section{Proof of Theorem~\ref{t:bf}\label{app:bf}}

\section{Additional Examples}
\subsection{A Reversible Protocol with  Choices}\label{app:choices}
%\jp{to do}
We use a simple binary (two-party) protocol between a Buyer (\pB) and a Seller (\pS) to further illustrate our process framework, in particular to showcase reversibility of labeled choices. Consider the following global type:
\begin{align*}
G = ~&  \gtcom{B}{S}{\mathsf{title}}{\gtcom{S}{B}{\mathsf{price}}{\\
&{\gpart{S}\to \gpart{B}\{\mathbf{ok}: \gtcom{B}{S}{\mathsf{addr}}{\gtcom{S}{B}{\mathsf{date}}{\gend} \,; 
 \mathbf{quit}: \gend\}
}}}}
\end{align*}
This way, after receiving a title from Buyer, Seller replies with the price of the requested item; subsequently, a  choice indicated by labels  $\mathbf{ok}$ and $\mathbf{quit}$ takes place: Buyer can select whether to continue with the transaction or to conclude it.
The projection of $G$ onto local types are:
\begin{align*}
\tproj{G}{\pS} ~= ~& \ltinp{B}{\mathsf{title}}{\ltout{B}{\mathsf{price}}{\\ &\gpart{B}\&\{\mathbf{ok}: \ltinp{B}{\mathsf{addr}}{\ltout{B}{\mathsf{date}}{\lend}} \, ; \, \mathbf{quit}: \lend \}}}\\
%
\tproj{G}{\pB} ~= ~& \ltout{S}{\mathsf{title}}{\ltinp{S}{\mathsf{price}}{\\ &\gpart{S}\oplus\{\mathbf{ok}: \ltout{S}{\mathsf{addr}}{\ltinp{S}{\mathsf{date}}{\lend}} \, ; \, \mathbf{quit}: \lend \}}}
\end{align*}
Possible implementations for the participants are as follows:
\begin{align*}
\text{Seller} & =  \bout{a}{x:\tproj{G}{\pS}}\binp{x}{title}\bout{x}{quote}\\
&\bbra{x}{\mathbf{ok}: \binp{x}{addr}\bout{x}{date} \,;\,\mathbf{quit}:\inact}\\
\text{Buyer} & =  \binp{a}{y:\tproj{G}{\pB}}\bout{y}{title}\binp{y}{quote}\\
&\bsel{y}{\mathbf{ok}: \bout{y}{addr}\binp{y}{date} \,;\,\mathbf{quit}:\inact}
\end{align*}
The whole system, given by configuration $M$ below, is obtained by placing these process implementations in appropriate locations:
$$
M = \myloc{\loc_1}{\text{Seller}} 
\Par
\myloc{\loc_2}{\text{Buyer}}
$$
We then may have:
\begin{align*}
&M \trans{\fw}\\
& \news{s}(\,  \np{\key{\loc_1}{\pS}}{ \conf{\inact}{ \bbra{\epS}{\mathbf{ok}: \binp{\epS}{addr}\bout{\epS}{date}\inact \,;\,\mathbf{quit}:\inact} }} \Par \\
&\hmoni{s_\pS}{\myctx{T_\text{1}}{\past \gpart{B}\&\{\mathbf{ok}: \ltinp{B}{\mathsf{addr}}{\ltout{B}{\mathsf{date}}{\lend}} \, ; \, \mathbf{quit}: \lend \}}}{x_1}{\store_1} \Par \\
&
\np{\key{\loc_2}{\pB}}{ \conf{\inact}{ \bsel{\epB}{\mathbf{ok}: \binp{\epB}{addr}\bout{\epB}{date}\inact \,;\,\mathbf{quit}:\inact} }} \Par \\
&\hmoni{s_\pB}{\myctx{S_\text{1}}{\past \gpart{S}\oplus\{\mathbf{ok}: \ltout{S}{\mathsf{addr}}{\ltinp{S}{\mathsf{date}}{\lend}} \, ; \, \mathbf{quit}: \lend \}}}{x_2}{\store_2} \Par \\
& \codah{s}{h_1}{\emp}{}~) = M_1
\end{align*}
%
where $M_1$ is the configuration obtained from $M$ once the two participants have initiated the session and exchanged the title and the corresponding price. Above, $x_1$ and $x_2$ are the free variables of \pS and \pB after the first three interactions; also, $\store_1$ and $\store_2$ represent their respective stores. Queue $h_1$ contains the two messages related to $title$ and $price$.
The context types are: 
$$
\myctxr{\ctx{T}_1}{\bullet} = \ltinp{B}{\mathsf{title}}{\ltout{B}{\mathsf{price}}}{\bullet} \qquad
 \myctxr{\ctx{S}_1}{\bullet} = \ltout{S}{\mathsf{title}}{\ltinp{S}{\mathsf{price}}}{\bullet}
 $$
 In $M_1$, Buyer can decide either (a) to accept the suggested price and continue with the prescribed protocol or (b) to refuse it and exit. The first possibility may proceed using Rule~\fwcolor{\textsc{(Sel)}} as follows:
%
\begin{align*}
&M_1 \fw\\
&\news{s}(\,\np{\key{\loc_2}{\pB}}{ \conf{\inact, \bsel{\epB}{\mathbf{quit}: \inact}}{  \binp{\epB}{addr}\bout{\epB}{date}\inact  }} \Par \\
&\hmoni{s_\pB}{\myctx{S_\text{1}}{ \gpart{S}\oplus\{\mathbf{ok}: \past\ltout{S}{\mathsf{addr}}{\ltinp{S}{\mathsf{date}}{\lend}} \, ; \, \mathbf{quit}: \lend \}}}{x_2}{\store_2} \Par \\
&\codah{s}{h_1}{\valueq{\pB}{\pS}{\mathbf{ok}} } \Par N_1~) = M_2
\end{align*} 
where $N_1$  contains the rest of the Seller process and monitor of $M_1$. 
As we can see, in $M_2$ the cursor $\past$ of the Buyer monitor has been moved into the choice. 
Moreover. the process stack of Buyer is updated in order to register the discarded branch of the choice (i.e., the branch involving  label  $\textbf{quit}$). From $M_2$,  Seller can consume the message on top of the queue (which details the choice by \pB), or the Buyer can revert its choice. 
In the first case we have the following, using Rule~\fwcolor{\textsc{(Bra)}}:
\begin{align*}
&M_2 \fw\\
&\news{s}(\,\np{\key{\loc_1}{\pS}}{ \conf{\inact , \bbra{\epS}{\mathbf{quit}:\inact}}{ \binp{\epS}{addr}\bout{\epS}{date}\inact  }} \Par \\
&\hmoni{s_\pS}{\myctx{T_\text{1}}{ \gpart{B}\&\{\mathbf{ok}: \past\ltinp{B}{\mathsf{addr}}{\ltout{B}{\mathsf{date}}{\lend}} \, ; \, \mathbf{quit}: \lend \}}}{x_1}{\store_1} \Par \\
&
\np{\key{\loc_2}{\pB}}{ \conf{\inact , \bsel{\epB}{\mathbf{quit}: \inact}}{  \binp{\epB}{addr}\bout{\epB}{date}\inact  }} \Par \\
&\hmoni{s_\pB}{\myctx{S_\text{1}}{ \gpart{S}\oplus\{\mathbf{ok}: \past\ltout{S}{\mathsf{addr}}{\ltinp{S}{\mathsf{date}}{\lend}} \, ; \, \mathbf{quit}: \lend \}}}{x_2}{\store_2} \Par \\
&\codah{s}{h_1\cons \valueq{\pB}{\pS}{\mathbf{ok}}}{\emp } ~) = M_3
\end{align*}
In the second case, we can revert the labeled choice by using 
Rule~\bkcolor{\textsc{(RollC)}} from $M_3$ first, 
and then using 
Rules~\bkcolor{\textsc{(RBra)}} and \bkcolor{\textsc{(RSel)}}
in a decoupled fashion.


\section{Omitted Proofs}
\subsection{Proof of Theorem ~\ref{t:bf}}\label{app:bf}

We repeat the statement in Page~\pageref{t:bf}:

\begin{tm}{\ref{t:bf}}
For any atomic reachable configuration $M$, we have that $M \congruence\bfbw M$.
\end{tm}

\begin{proof}
First, notice that showing $\ctx{C}[M]\bfbw\ctx{C}[M]$ is similar to show 
$M_1 \bfbw M_1$ with $M_1 = \ctx{C}[M]$.
This allows us to just focus on the ``hole'' of the context. 
It is then sufficient to show that the following relation is a 
bf weak bisimulation. 
\begin{align*}
	\Re =\{ (M,N) \st  M \trans{\fw} N \text{ via Rules~\textsc{Out} or \textsc{Sel}} \wedge   
	\\
	M \trans{\bk} N \text{ via Rules~\textsc{ROut} or \textsc{RSel}} \} 
\end{align*}
Clearly, $(M, M) \in \Re$. We consider the requirements in Def.~\ref{d:bf}.

Let us first consider barbs. Suppose that $M$ challenges $N$ with a barb, 
we distinguish two cases: $N$ is stable or not.
If
 $\stable(N)$  then $N$  has the same barb. Otherwise,  if $\lnot\stable(N)$,
 by  Corollary~\ref{lbl:corollary_finish} 
 there exists an $N_1$ such that
 $N\trans{\red} N_1$ and $\stable(N_1)$.
 Since $M \trans{\red} N$ 
  we may derive $M\trans{\red} N_1$ with both stable configurations. 
  By applying Theorem~\ref{theo:correspond} on $M\trans{\red} N_1$ we infer $M\trans{\reda} N_1$;
  then, by
 applying the Loop Lemma (Lemma~\ref{lemma:loop})  we further infer $N_1\trans{\reda} M$. 
 Using again Theorem~\ref{theo:correspond} we infer that $N_1\trans{\red} M$; 
 since we have deduced that $N\trans{\red} N'\trans{\red} M$,
 we know that $N$ weakly matches all the barbs of $M$, as desired. 
 Suppose now that $N$ challenges $M$ with a barb.
 We proceed similarly as above:
  if $\stable(M)$ then $M$ has the same barb; otherwise, if $\lnot\stable(M)$, since $M\trans{\red} N$, by Corollary~\ref{lbl:corollary_finish} we have that $M\trans{\red} N \trans{\red}N_1$, with $\stable(N_1)$.
 Let us note that the reductions in $N\trans{\red} N_1$ do not add barbs to $N_1$: they only finalize ongoing synchronizations; by definition of barbs (Def.~\ref{lbl:barb}) parties involved in ongoing rollbacks do not contribute to barbs. We can conclude by applying Theorem~\ref{theo:correspond} and deriving $M\trans{\reda} N_1$, which has the same barbs of $N$, as desired. 
 
 % and has the same barbs of $N_1$ since messages and branches involved in ongoing backward steps are not considered barbs (Definition~\ref{lbl:barb}).
 
 Let us now consider reductions. We will just focus on synchronizations due to input/output and branching/selection reduction steps, since 
 these are the cases in which $\red$ and $\reda$ differ; indeed, reductions due to Rules~\textsc{Spawn} and \textsc{Beta} can be trivially matched. There are two cases: $M\fwa M_1$ and $M\bka M_1$.
 In the first case, as  we distinguish two sub-cases: either $N$ has already started the synchronization or not. In the first case, $N$ can conclude the step: $N\fw N'$. Now we have that
 $M{\fws} N\fw N'$. Thanks to Lemma~\ref{lemma:swap} we can rearrange such a reduction sequence as follows: $M\fw\fw M_1{\fws} N'$. We then have that the pair $(M_1,N')\in \Re$, as desired. In the second case,
 $N$ can match the step with 2 reductions: $N\fw \fw N'$. Also in this case we can rearrange the reduction 
 sequence so as to obtain $M\fw\fw M_1\trans{\fw} N'$, with  $(M_1,N')\in \Re$, as desired. 
The second case is when $M\bka M_1$ (i.e., the challenge is a backward move) and is handled similarly. 
 
We now consider challenges from $N$, focusing only on synchronizations, just as before.
 %we will just focus on communications steps, since the case of \textsc{Spawn} and \textsc{Beta} is trivially matched.  
 If $N\fw N'$, we distinguish two cases: whether the reduction finalizes ends an ongoing  input/output and branching/selection, or it opens a new one. 
   In the second case $M$ matches the move with an idle move, i.e.,
 $(M,N')\in \Re$. In the other case   we can rearrange the reduction $M{\fws}N\fw N'$ into a similar reduction sequence
 $M\trans{\red} N_1{\fws} N'$ with $\stable(N_1)$, and all reductions  in $N_1\fws N'$ just start new synchronizations. 
 Thanks to Theorem~\ref{theo:correspond}, $M$ can mimick the same reduction to $N_1$, i.e., $M\trans\fwa N_1$, and we have that $(N_1,N')\in \Re$, as desired. 
 The case in which $N \bk N'$ (i.e., the challenge is a backward move) is similar. This concludes the proof.
\end{proof}

\subsection{Appendix to \S\,\ref{ss:conn}}\label{app:corrgc}
\paragraph{Well-formed Process Implementations of a Local Type\label{app:adeq}}
The results in \S\,\ref{ss:conn} rely on \emph{well-formedness} of a process $P$ with respect to a local type $T$.
Figure~\ref{f:wft} reports a very simple system for decreeing well-formedness.
It is inspired by the type system for processes defined in~\cite{DBLP:journals/fac/CastellaniDP16};
clearly, more sophisticated systems, such as variants of those in~\cite{tlca07,KPY2016}, can be considered.
We rely on two judgments: 
\begin{itemize}
\item $\vdash V:: U$ says that $V$ is a well-formed (i.e. valid) value of type $V$.
\item $\Gamma \vdash P :: x:T$ says that  $P$ implements a single session with local type $T$ along variable $x$, relying 
on type assignments for name variables and recursive variables declared in $\Gamma$. 
\end{itemize}
We will write $\ladeq{P}{T}{x}$ if and only iff 
$\emptyset \vdash P :: x:T$.
This notion of well-formedness can be extended to relate configurations and local types with history; see Figure~\ref{f:wfc}.

\subsection{Proof of Theorem~\ref{t:corrgc}}
We write 
$\parties{\gth{H}}$ to denote the set of participants in a global type with history $\gth{H}$. 
%Also, we rely on the extension of projection to global types with history
%(cf. Figure~\ref{f:projext}).
The following proposition details the shape of configurations 
that are reachable from a configuration that
initially implements a global type with history.
In particular, monitor tags can be full $\bkcolor{\rmark}$ or empty $\normark$, and so if 
$\adeq{M}{\gth{H}}$ then $M$ may not be stable:

\begin{proposition}\label{p:shape}
Let $\adeq{M}{\gth{H}}$ 
with $\parties{\gth{H}}= \{\p_1,\cdots,\p_n\}$.
Then we have 
\begin{align*}
M\equiv  
\news{s,\widetilde{n}} \Big(\, 
\prod_{i \in\{1,\cdots,n\}} \np{\key{\loc_i}{\p_i}}{ \conf{\stack{C}_i}{Q_i}} \Par 
\\
\monig{s_{\p_i}}{\myctxr{\ctx{T}_i}{ \past S_i}}{\widetilde{x_i}}{\store_i}  \Par \codah{s}{h_1^i}{h_2^i}\Big)
\end{align*}
with 
%$\ladeq{P_i}{\tproj{G}{\p_i}}{x}$, for all $i \in\{1,\!\cdots\!,n\}$, 
$\ladeq{{\conf{\stack{C}_i}{Q_i}}}{\myctxr{\ctx{T}_i}{ \past S_i}}{\key{s}{\p_i}}$ (cf. Figure~\ref{f:wfc}), for all $i \in\{1,\!\cdots\!,n\}$, 
for some 
stores $\store_1, \ldots, \store_n$,
process stacks $\stack{C}_1, \ldots, \stack{C}_n$.
type contexts $\ctx{T}_1, \ldots, \ctx{T}_n$,
local types $S_1, \ldots, S_n$,
variables $\widetilde{x_1}, \ldots, \widetilde{x_n}$,
and 
queues $h_1^1, h_2^1, \ldots, h_1^n, h_2^n$.
\end{proposition}
\begin{proof}
Immediate from Definition~\ref{d:ic} (reachable configuration), Definition~\ref{d:ii} (``initially implements''),
and the reduction semantics $\red$.
\end{proof}


%\jp{This is the revised statement - please check and move to the main body if OK. 
%Recall that we write $M \bkk M'$ to denote a sequence of $j \geq 0$ reduction steps (if $j=0$ then $M = M'$).
%We repeat the statement in Page~\pageref{t:corrgc}:
%\begin{tm}{\ref{t:corrgc}}
%Let $\mathsf{H}$  be a reachable, first-order global type with history (cf. \S\,\ref{ss:chore}).
%\begin{enumerate}[a)]
%\item If $\adeq{M}{\gth{H}}$ and $\gth{H} \fwg \gth{H}'$  then  $M \fw M'$  and $\adeq{M'}{\gth{H'}}$, for some $M'$.
%If $\adeq{M}{\gth{H}}$ and $\gth{H} \bkg \gth{H}'$ then $M \bk^k M'$ (with $k =1$ or $k=2$) and $\adeq{M'}{\gth{H'}}$, for some $M'$.
%
%%\item If $\adeq{M}{\gth{H}}$ and $M \fw N$ then 
%% $\gth{H} \fwg \gth{H}'$  and $\adeq{N}{\gth{H'}}$, for some  $\gth{H}'$.
%% If $\adeq{M}{\gth{H}}$ 
%% and $M \bk N'$ then  
%% $N' \bk^k N$ (with $k =0$ or $k=1$),
%% $\gth{H} \bkg \gth{H}'$,
%% and $\adeq{N}{\gth{H'}}$, for some  $N, \gth{H}'$.
%\item If $\adeq{M}{\gth{H}}$ and $M \fw N$ then 
% $\gth{H} \swap \gth{H}'\fwg \gth{H}''$  and $\adeq{N}{\gth{H}''}$, for some  $\gth{H}'$, $\gth{H}''$.
% If $\adeq{M}{\gth{H}}$ 
% and $M \bk N'$ then  
% $N' \bk^k N$ (with $k =0$ or $k=1$),
% $\gth{H} \swap \gth{H}' \bkg \gth{H}''$,
% and $\adeq{N}{\gth{H'}}$, for some  $N$, $\gth{H}'$, $\gth{H}''$.
%\end{enumerate} 
%\end{tm}

%\jp{This is Thursday's statement:}
%
%\begin{theorem}
%Let $\mathsf{H}$  be a reachable global type with history (cf. \S\,\ref{ss:chore}).
%\begin{enumerate}[a)]
%\item If $\adeq{M}{\gth{H}}$ and $\gth{H} \fwg \gth{H}'$ (resp. $\gth{H} \bkg \gth{H}'$) then  there exists $M'$ such that $M \fw M'$ (resp. $M \bk\bk M'$) and $\adeq{M'}{\gth{H'}}$.
%\item If $\adeq{M}{\gth{H}}$ and $M \fw N$ (resp. $M \bk\bk N$) then there exists $\gth{H}'$
%such that 
% $\gth{H} \fwg \gth{H}'$ (resp. $\gth{H} \bkg \gth{H}'$) and $\adeq{N}{\gth{H'}}$.
%%$N' \bk N$,
%%$\adeq{N}{\gth{H'}}$, 
%% $\gth{H} \bkg \gth{H}'$.
%\end{enumerate} 
%\end{theorem}

%%% ==== START QUEUE EQUIVALENCE
The following congruence allows us to (silently) modify the order of the messages in the queue in a consistent way: 
\begin{definition}[Equivalence on message queues]
We define the structural equivalence on queues, denoted $\equivq$, as follows:
\begin{align*}
h\cons \valueq{\p_1}{\q_1}{\anyv_1} \cons \valueq{\p_2}{\q_2}{\anyv_2}  \cons h'
\equivq 
\qquad \qquad \qquad
\\
%\vspace{5mm}
\qquad \qquad \qquad
h\cons \valueq{\p_2}{\q_2}{\anyv_2} \cons \valueq{\p_1}{\q_1}{\anyv_1} \cons h'
\end{align*}
whenever $\p_1 \neq \p_2 \land \q_1 \neq \q_2$.
Equivalence $\equivq$ extends  to configurations as expected.
\end{definition}
%%% ==== END QUEUE EQUIVALENCE

We may now have:

\begin{proof}[Proof of Theorem~\ref{t:corrgc} (Sketch)]
The proof of Part (a) proceeds by induction on the transitions $\gth{H} \fwg \gth{H}'$ and $\gth{H} \bkg \gth{H}'$, with a case analysis on the last applied rule.
For the forward case we have a one-to-one correspondence; there are four possible transitions at the level of global types:
a transition derived using Rule~\textsc{(FVal1)} is matched by $M$   using Rule~\textsc{(Out)};  
a transition derived using Rule~\textsc{(FVal2)} is matched by $M$  using Rule~\textsc{(In)};  
a transition derived using Rule~\textsc{(FCho1)} is matched by $M$   using Rule~\textsc{(Sel)};  
 a transition derived using Rule~\textsc{(FCho2)} is matched by $M$  using Rule~\textsc{(Bra)}.
The analysis for the backward case is similar, but  
before matching  the transition $\gth{H} \bkg \gth{H}'$, 
 we may require an additional reduction step from $M$, depending on the tag 
 of the corresponding monitor. We use Prop.~\ref{p:shape} to determine this tag.
 If the tag is $\normark$, then a reduction  (using Rule~\textsc{(RollS)} or \textsc{(RollC)})
 is required 
 in order to have a full tag $\rmark$, as needed by all relevant backward reduction rules ($j=2$).
 Otherwise, if the tag is already $\rmark$ from a previous reduction then no additional step is needed ($j=1$).
 Once the tag is full, the transition  is matched as follows:
a transition derived using Rule~\textsc{(BVal1)} is matched by $M$  using Rule~\textsc{(ROut)};  
a transition derived using Rule~\textsc{(BVal2)} is matched by $M$   using Rule~\textsc{(RIn)};  
a transition derived using Rule~\textsc{(BCho1)} is matched by $M$   using Rule~\textsc{(RSel)};  
a transition derived using Rule~\textsc{(BCho2)} is matched by $M$   using Rule~\textsc{(RBra)}.

\smallskip

The proof of Part (b) 
proceeds by induction on transitions $M \fw N$ and $M \bk N$, with a case analysis on the last applied rule, following similar lines.
There are two main cases: 
\begin{enumerate}[(i)]
\item There is exactly one reduction from $M$  involving the participants that appear at the top-level in $\gth{H}$ and can evolve. 
\item There are one or more reductions from $M$ to $N_i$ whose involved participants cannot be found at the top-level in $\gth{H}$.
\end{enumerate}

While in case~(i) the proof follows the analysis for Part~(a), 
in case (ii) we use $\swap$ on $\gth{H}$ to obtain 
behavior-preserving transformations $\gth{H}_i$ of $\gth{H}$ in which the participants involved in the reductions
 ($M \fw N_i$ or $M \bk N_i$) appear at the top-level.
 Such transformations exist, because of assumption $\adeq{M}{\gth{H}}$.
This way, reductions from $M$ can be matched by $\gth{H}$ up to swapping; after all the independent communication actions 
have been performed and matched (there are finitely many of them), one obtains $M'$, $\gth{H}$ such that  $\adeq{M'}{\gth{H}''}$.
 
In both (i) and (ii), the analysis of a backwards reduction from $M$ relies on 
Prop.~\ref{p:shape} to determine the relevant tag involved. 
If the  tag in $M$ is $\rmark$ then
a reduction $M \bk N'$ was derived using Rules~\textsc{(ROut)}, \textsc{(RIn)}, \textsc{(RSel)}, or \textsc{(RBra)} and it is easy to show that it 
corresponds directly to one transition from $\gth{H}$ ($j=0$).
When the reduction is derived using Rules~\textsc{(RollS)} or \textsc{(RollC)} (because the corresponding tag in $M$ is $\normark$),  there is no corresponding transition from $\gth{H}$
and an extra reduction (using Rules~\textsc{(ROut)}, \textsc{(RIn)}, \textsc{(RSel)}, or \textsc{(RBra)}, which become enabled thanks to Rules~\textsc{(RollS)} and \textsc{(RollC)}) is required 
to actually match the transition ($j=1$).
It is worth noticing that 
due to the simplicity of our well-formed processes/configurations (and our focus on first-order global types), 
reduction  $M \fw N$ does not involve 
Rule~\textsc{(Spawn)} (for well-formed processes are single-threaded) nor
Rule~\textsc{(Beta)} (for ($\appl{V}{w})$ is a well-formed value but not a well-formed process).
Similarly, $M \bk N$ does not involve Rules~\textsc{(RSpawn)} and \textsc{(RBeta)}.
\end{proof}

\begin{figure}[!t]
{\small
\begin{mathpar}
\inferrule
{  }{
\Gamma \vdash \inact :: x:\lend}
\qquad
\inferrule
{  }{
\Gamma, X:T \vdash X :: x:T}
\qquad
\inferrule
{
\Gamma, X:T \vdash P :: x:T}
{\Gamma \vdash \mu X.P :: x:T}
\\
\inferrule{\Gamma \vdash P :: x:T \quad  \vdash V::U}
{\Gamma \vdash \bout{x}{V}{P} :: x:\typeOut{\p}{U}.T}
\quad
\inferrule{\Gamma, y:U \vdash P :: x:T}
{\Gamma \vdash \binp{x}{y}{P} :: x:\typeIn{\p}{U}.T}
\\
\inferrule{\forall i \in  \{1, \ldots, n\}.(\Gamma \vdash P_i :: x:T_i)}
{\Gamma \vdash  \bsel{x}{\lbl_i. P_i}_{i\in \{1, \ldots, n\}} :: x:\ltsel{\q}{\lbl_i}{T_i}{i}{\{1, \ldots, n\}}}
\\
\inferrule{\forall i \in  \{1, \ldots, n\}.(\Gamma \vdash P_i :: x:T_i)}
{\Gamma \vdash  \bbra{x}{\lbl_i : P_i}_{i\in \{1, \ldots, n\}} :: x:\ltbra{\q}{\lbl_i}{T_i}{i}{\{1, \ldots, n\}}}
\end{mathpar}
}
\vspace{-4mm}
\caption{Well-formed processes with respect to a local type.\label{f:wft}}
\end{figure}

%\begin{figure}[t!]
%{\small
%\begin{align*}
%\tproj{\gtcom{p}{\!\!\past q}{U}{G}}{\gpart{r}} & = 
%\begin{cases}
%\ltout{\q}{U}{\past (\tproj{G}{\gpart{r}})} & \text{if $\gpart{r} = \gpart{p}$} \\
%\past \ltinp{\p}{U}{(\tproj{G}{\gpart{r}})} & \text{if $\gpart{r} = \gpart{q}$} \\
%(\tproj{G}{\gpart{r}}) &  \text{if $\gpart{r} \neq \gpart{q}, \gpart{r} \neq \gpart{p}$}
%\end{cases}
%\\
%\tproj{\gtcom{p}{q}{U}{\past G}}{\gpart{r}} & = 
%\begin{cases}
%\ltout{\q}{U}{\past (\tproj{G}{\gpart{r}})} & \text{if $\gpart{r} = \gpart{p}$} \\
% \ltinp{\p}{U}{\past(\tproj{G}{\gpart{r}})} & \text{if $\gpart{r} = \gpart{q}$} \\
%(\tproj{G}{\gpart{r}}) &  \text{if $\gpart{r} \neq \gpart{q}, \gpart{r} \neq \gpart{p}$}
%\end{cases}
%\\
%\tproj{\gpart{p}\to\!\!\past\gpart{q}:\{\lbl_i:G_i \,;\, \lbl_j:G_j\}_{i \in I\setminus j}}{\gpart{r}} & = 
%\begin{cases}
%\ltselp{\q}{\lbl_i:\tproj{G_i}{\gpart{r}} \;;\; \lbl_j:\tproj{G_j}{\gpart{r}}}{i}{I\setminus j}
%& \text{if $\gpart{r} = \gpart{p}$} \\
%\past \ltbra{\p}{\lbl_i}{\tproj{G_i}{\gpart{r}}}{i}{I} & \text{if $\gpart{r} = \gpart{q}$} \\
%(\tproj{{G_1}}{\gpart{r}}) &  \text{if $\gpart{r} \neq \gpart{q}, \gpart{r} \neq \gpart{p}$}
%\end{cases}
%\\
%\tproj{\gpart{p}\to\gpart{q}:\{\lbl_i:G_i \,;\, \lbl_j:\past G_j\}_{i \in I\setminus j}}{\gpart{r}} & = 
%\begin{cases}
%\ltselp{\q}{\lbl_i:\tproj{G_i}{\gpart{r}} \;;\; \lbl_j:\tproj{G_j}{\gpart{r}}}{i}{I\setminus j}
%& \text{if $\gpart{r} = \gpart{p}$} \\
% \ltbrap{\p}{\lbl_i:\tproj{G_i}{\gpart{r}} \;;\; \lbl_j:\tproj{G_j}{\gpart{r}}}{i}{I\setminus j} & \text{if $\gpart{r} = \gpart{q}$} \\
%(\tproj{{G_1}}{\gpart{r}}) &  \text{if $\gpart{r} \neq \gpart{q}, \gpart{r} \neq \gpart{p}$}
%\end{cases}
%\\
%\tproj{(\past G)}{\gpart{r}} &= \past (\tproj{G}{\gpart{r}})
%\qquad
%\tproj{(G \past )}{\gpart{r}} =  (\tproj{G}{\gpart{r}})\past
%\end{align*}
%}
%\caption{Projection of a global type with history $\mathsf{H}$ onto a participant $\gpart{r}$.\label{f:projext}}
%\end{figure}


\begin{figure}[!t]
{\small
\begin{mathpar}
\inferrule
{\ladeq{P}{T}{x}}
{\ladeq{\conf{\inact}{P}}
{\past T}{x}}
\\
\inferrule{\ladeq{\conf{\stack{C}}{\bout{x}{V}{P}}}{\myctxr{\ctx{T}}{\past  \ltout{\q}{U}{S}}}{x}}
{\ladeq{\conf{\stack{C}}{{P}}}{\myctxr{\ctx{T}}{\ltoutp{\q}{U}{S}}}{x}}
\qquad
\inferrule{\ladeq{\conf{\stack{C}}{\binp{x}{y}{P}}}{\myctxr{\ctx{T}}{\past  \ltinp{\q}{U}{S}}}{x}}
{\ladeq{\conf{\stack{C}}{{P}}}{\myctxr{\ctx{T}}{\ltinpp{\q}{U}{S}}}{x}}
\\
\inferrule{\ladeq{\conf{\stack C}{\bsel{x}{\lbl_i. P_i}_{i\in I}}}{\myctxr{\ctx{T}}{\past \ltsel{\q}{\lbl_j}{S_j}{j}{J}}}{x} \quad w \in I,J}
{\ladeq{\conf{\stack C , \bsel{x}{\lbl_l.P_l}_{l\in I\setminus w} }{P_w}}{\myctxr{\ctx{T}}{ \ltselp{\q}{\lbl_j:S_j \, , \, \lbl_w:\past S_w}{j}{J\setminus w}} }{x}}
\\
\inferrule{\ladeq{\conf{\stack C}{\bbra{x}{\lbl_i. P_i}_{i\in I}}}{\myctxr{\ctx{T}}{\past \ltbra{\q}{\lbl_j}{S_j}{j}{J}}}{x} \quad w \in I,J}
{\ladeq{\conf{\stack C , \bbra{x}{\lbl_l.P_l}_{l\in I\setminus w} }{P_w}}{\myctxr{\ctx{T}}{ \ltbrap{\q}{\lbl_j:S_j \, , \, \lbl_w:\past S_w}{j}{J\setminus w}} }{x}}
\\
\inferrule{\ladeq{\conf{\stack{C}}{{P}}}{\myctxr{\ctx{T}}{\ltoutp{\q}{U}{S}}}{x} \quad \vdash V :: U}
{\ladeq{\conf{\stack{C}}{\bout{x}{V}{P}}}{\myctxr{\ctx{T}}{\past  \ltout{\q}{U}{S}}}{x}}
\\
\inferrule{\ladeq{\conf{\stack{C}}{{P}}}{\myctxr{\ctx{T}}{\ltinpp{\q}{U}{S}}}{x} \quad y:U \vdash P :: S}
{\ladeq{\conf{\stack{C}}{\binp{x}{y}{P}}}{\myctxr{\ctx{T}}{\past  \ltinp{\q}{U}{S}}}{x}}
\\
\inferrule
{\ladeq{\conf{\stack C , \bsel{x}{\lbl_l.P_l}_{l\in I} }{P_w}}{\myctxr{\ctx{T}}{ \ltselp{\q}{\lbl_j:S_j \, , \, \lbl_w:\past S_w}{j}{J}} }{x}}
{\ladeq{\conf{\stack C}{\bsel{x}{\lbl_i. P_i}_{i\in I \cup w}}}{\myctxr{\ctx{T}}{\past \ltsel{\q}{\lbl_j}{S_j}{j}{J \cup w}}}{x}}
\\
\inferrule
{\ladeq{\conf{\stack C , \bbra{x}{\lbl_l.P_l}_{l\in I} }{P_w}}{\myctxr{\ctx{T}}{ \ltbrap{\q}{\lbl_j:S_j \, , \, \lbl_w:\past S_w}{j}{J}} }{x}}
{\ladeq{\conf{\stack C}{\bbra{x}{\lbl_i. P_i}_{i\in I \cup w }}}{\myctxr{\ctx{T}}{\past \ltbra{\q}{\lbl_j}{S_j}{j}{J \cup w}}}{x}}
\end{mathpar}
}
\caption{Well-formed configurations with respect to a local type with history.\label{f:wfc}}
\end{figure}


macros.tex
% !TEX root = revchor.tex


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Contents
% --------

% 1.  Formating
% 2.  Maths - Theorems
% 3.  The pi Calculus
% 4.  Session Syntax
% 5.  Subject Reduction
% 6.  Global Session Types
% 7.  Global Session Types Equivalence
% 8.  Projection
% 9.  Local Session Types
% 10. Behavioural Theory
% 11. Typed Transitions - Reductions
% 12. Typed Relations
% 13. Confluence Determinacy
% 14. Mapping
% 15. pi Constructs
% 16. LN Transform
% 17. General Types Processes Names Sessions ETC
% 18. newtheorem - newenvironment
% 19. Misc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                       FORMATING
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Symbols
\newcommand{\semicolon}{:}
%\newcommand{\colon}{;}
\newcommand{\lrangle}[1]{\langle #1 \rangle}
\newcommand{\blrangle}[1]{\big\langle #1 \big\rangle}

%Tags
\newcommand{\parenthtext}[1]{(\textrm{\small #1})}
\newcommand{\brtext}[1]{[\textrm{\small #1}]}
\newcommand{\textinmath}[1]{\textrm{#1}}
\newcommand{\srule}[1]{\parenthtext{#1}}
\newcommand{\strule}[1]{\textrm{#1}}
\newcommand{\stypes}[1]{{\footnotesize \parenthtext{#1}}}
\newcommand{\ltsrule}[1]{{\footnotesize \lrangle{\textrm{#1}}}}
\newcommand{\eltsrule}[1]{{\footnotesize [\textrm{#1}]}}
\newcommand{\trule}[1]{{\footnotesize\brtext{#1}}}
\newcommand{\orule}[1]{{\scriptsize{\brtext{#1}}}}
\newcommand{\mrule}[1]{{\footnotesize{\parenthtext{#1}}}}

\newcommand{\iftag}{{\textrm{if }}}

% General
\newcommand{\noi}{\noindent}
\newcommand{\Hline}{\rule{\linewidth}{.5pt}}
\newcommand{\Hlinefig}{\rule{\linewidth}{.5pt}\vspace{-4mm}}
\newcommand{\myparagraph}[1]{\noindent{\textbf{#1}\ }}
\newcommand{\jparagraph}[1]{\paragraph{\textbf{#1}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                       MATHS - THEOREMS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\newtheorem{notation}[definition]{Notation}

% BNF form
\newcommand{\bnfis}{\;\;::=\;\;}
\newcommand{\bnfbar}{\;\;\;|\;\;\;}
\newcommand{\sbnfbar}{\;|\;}

% Proof
\newcommand{\Case}[1]{\noi {\bf Case: }#1\\}
\newcommand{\proofend}{\qed}
%\newcommand{\proofend}{}
\newcommand{\Proof}{\noi {\bf Proof: }}

% Logic
\newcommand{\LogAnd}{\texttt{ and }}
\newcommand{\LogOr}{\texttt{ or }}

% Induction

\newcommand{\basic}{\noi {\bf Basic Step:}\\}
\newcommand{\inductive}{\noi {\bf Inductive Hypothesis:}\\}
\newcommand{\induction}{\noi {\bf Induction Step:}\\}

% Tree

\newcommand{\tree}[2]{
\ensuremath{\displaystyle
		\frac
		{
			%%\raisebox{0.0mm}{$\displaystyle{#1}$}
			#1
			%\vspace{0mm}
		}{
			%\vspace{2mm}
			#2
			%\raisebox{-0.4mm}{$\displaystyle{#2}$}
		}
	}
}


%\newcommand{\tree}[2]{
%\begin{prooftree}
%	#1
%	\justifies
%	#2
%\end{prooftree}
%}

\newcommand{\treeusing}[3]{
\begin{prooftree}
	#1
	\justifies
	#2
	\using
	#3
\end{prooftree}}

% Vectors
\newcommand{\vect}[1]{\tilde{#1}}
\newcommand{\mytilde}[1]{\widetilde{#1}}

% Functions - Set theory
\newcommand{\set}[1]{\{#1\}}
\newcommand{\es}{\emptyset}
\newcommand{\maxset}[1]{\max(#1)}
\newcommand{\setbar}{\ \ |\ \ }
\newcommand{\tuple}[2]{(#1, #2)}
\newcommand{\suchthat}{\cdot}
\newcommand{\powerset}[1]{\mathcal{P}(#1)}
\newcommand{\product}{\times}

\newcommand{\eval}{\downarrow}

\newcommand{\setsubtr}[2]{#1 \backslash #2}

\newcommand{\func}[2]{#1(#2)}
\newcommand{\dom}[1]{\mathtt{dom}(#1)}
\newcommand{\codom}[1]{\mathtt{codom}(#1)}

\newcommand{\funcbr}[2]{#1\lrangle{#2}}

\newcommand{\entails}{\text{implies}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                        pi - CALCULUS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Free-Bound notation
\newcommand{\freev}[1]{\lrangle{#1}}
\newcommand{\boundv}[1]{(#1)}

% General pi calculus Syntax
\newcommand{\send}[1]{\overline{#1}}
\newcommand{\ol}[1]{\overline{#1}}
\newcommand{\receive}[1]{#1.}
\newcommand{\inact}{\mathbf{0}}
\newcommand{\If}{\sessionfont{if}\ }
\newcommand{\Then}{\sessionfont{then}\ }
\newcommand{\Else}{\sessionfont{else}\ }
\newcommand{\ifthen}[2]{\If #1\ \Then #2\ }
\newcommand{\ifthenelse}[3]{\ifthen{#1}{#2} \Else #3}
\newcommand{\Par}{\;|\;}
\newcommand{\news}[1]{(\nu\, #1)}
\newcommand{\newsp}[2]{(\nu\, #1)(#2)}
\newcommand{\varp}[1]{#1}
%\newcommand{\rvar}[1]{\mathcal{#1}}
\newcommand{\rvar}[1]{#1}
%\newcommand{\rec}[2]{\mu #1. #2}
\newcommand{\recp}[2]{\mu \rvar{#1}. #2}

\newcommand{\Def}{\sessionfont{def}\ }

\newcommand{\defeq}{\stackrel{\Def}{=}}

\newcommand{\repl}{\ast\,}
\newcommand{\parcomp}[2]{\prod_{#1}{#2}}

% Free-Bound-Names sets
\newcommand{\bn}[1]{\mathtt{bn}(#1)}
\newcommand{\fn}[1]{\mathtt{fn}(#1)}
\newcommand{\sn}[1]{\mathtt{sn}(#1)}
\newcommand{\ofn}[1]{\mathsf{ofn}(#1)}
\newcommand{\fv}[1]{\mathtt{fv}(#1)}
\newcommand{\bv}[1]{\mathtt{bv}(#1)}
\newcommand{\fs}[1]{\mathtt{fs}(#1)}
\newcommand{\fpv}[1]{\mathtt{fpv}(#1)}
\newcommand{\nam}[1]{\mathtt{n}(#1)}

%Subject - Object
\newcommand{\subj}[1]{\mathtt{subj}(#1)}
\newcommand{\obj}[1]{\mathtt{obj}(#1)}

% Relations
\newcommand{\relfont}[1]{\mathcal{#1}}
\newcommand{\rel}[3]{#1\ \relfont{#2}\ #3}

\newcommand{\scong}{\equiv}
\newcommand{\acong}{\scong_{\alpha}}
\newcommand{\wb}{\approx}
\newcommand{\fwb}{\approx^\mathtt{C}}
\newcommand{\hwb}{\approx^\mathtt{H}}
\newcommand{\swb}{\approx^{s}}
\newcommand{\wbc}{\approx}
\newcommand{\WB}{\approx}

\newcommand{\red}{\longrightarrow}
\newcommand{\Red}{\rightarrow\!\!\!\!\!\rightarrow}
\newcommand{\Redleft}{\leftarrow\!\!\!\!\!\leftarrow}

%\newcommand{\subst}[2]{\set{#1/#2 }}
\def\subst#1#2{\{\raisebox{.5ex}{\small$#1$}\! / \mbox{\small$#2$}\}}

% Context
\newcommand{\hole}{-}
\newcommand{\context}[2]{#1[#2]}
\newcommand{\Ccontext}[1]{\C[#1]}

% Expression Context
\newcommand{\Econtext}[1]{\E[#1]}

% Barbs
\newcommand{\barb}[1]{\downharpoonright_{#1}}
\newcommand{\Barb}[1]{\Downarrow_{#1}}
\newcommand{\nbarb}[1]{\not\downarrow_{#1}}
\newcommand{\nBarb}[1]{\not\Downarrow_{#1}}

% General
%\newcommand{\ESP}{\ensuremath{\mathbf{ESP}}}
\newcommand{\ESP}{\text{ESP}}
\newcommand{\ESPsel}{\ESP^+}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                        SESSION SYNTAX
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Session font
\newcommand{\sessionfont}[1]{\mathtt{#1}}
\newcommand{\vart}[1]{\mathsf{#1}}

% General Session symbols
\newcommand{\ssep}{;}
\newcommand{\shsep}{.}
\newcommand{\outses}{!}
\newcommand{\inpses}{?}
\newcommand{\selses}{\triangleleft}
\newcommand{\brases}{\triangleright}
\newcommand{\dual}[1]{\overline{#1}}
\newcommand{\cat}{\cdot}

\newcommand{\allstypes}{\mathcal{S}}

% Binary Session Syntax


\newcommand{\bacc}[2]{#1 \boundv{#2} \shsep}
\newcommand{\breq}[2]{\send{#1} \freev{#2} \shsep}
\newcommand{\bareq}[2]{\send{#1} \freev{#2}}

\newcommand{\breqt}[3]{\send{#1} \boundv{#2:#3} \shsep}
\newcommand{\bacct}[3]{#1 \boundv{#2:#3} \shsep}

\newcommand{\bout}[2]{#1 \outses \freev{#2} \shsep}
\newcommand{\bbout}[2]{#1 \outses \blrangle{#2} \shsep}
\newcommand{\binp}[2]{#1 \inpses \boundv{#2} \shsep}
\newcommand{\bselold}[2]{#1 \selses #2 \shsep}
\newcommand{\bsel}[2]{#1 \selses \set{#2}}

%\newcommand{\bout}[2]{#1 \outses \freev{#2} \ssep}
%\newcommand{\bbout}[2]{#1 \outses \blrangle{#2} \ssep}
%\newcommand{\binp}[2]{#1 \inpses \boundv{#2} \ssep}
%\newcommand{\bsel}[2]{#1 \selses #2 \ssep}
\newcommand{\bbra}[2]{#1 \brases \set{#2}}
\newcommand{\bbras}[2]{#1 \brases #2}
\newcommand{\bbraP}[1]{#1 \brases \lPi}

% Multiparty Session syntax

\newcommand{\role}[1]{[#1]}

\newcommand{\srole}[2]{#1\role{#2}}
\newcommand{\sqrole}[2]{#1^{[]}\role{#2}}

\newcommand{\fromto}[2]{\role{#1} \role{#2}}
\newcommand{\sfromto}[3]{#1\fromto{#2}{#3}}

\newcommand{\sout}[3]{\srole{#1}{#2} \outses \freev{#3} \ssep}
\newcommand{\sinp}[3]{\srole{#1}{#2} \inpses \boundv{#3} \ssep}
\newcommand{\sdel}[4]{\srole{#1}{#2} \outses \freev{\srole{#3}{#4}} \ssep}
\newcommand{\ssel}[3]{\srole{#1}{#2} \selses #3 \ssep}
\newcommand{\sbra}[3]{\srole{#1}{#2} \brases \set{#3}}
\newcommand{\sbras}[3]{\srole{#1}{#2} \brases #3}
\newcommand{\sbraP}[2]{\srole{#1}{#2} \brases \lPi}

\newcommand{\acc}[3]{#1 \role{#2} \boundv{#3} \shsep}
\newcommand{\req}[3]{\send{#1} \role{#2} \boundv{#3} \shsep}
\newcommand{\areq}[3]{\send{#1} \role{#2} \freev{#3}}

\newcommand{\out}[4]{\sfromto{#1}{#2}{#3} \outses \freev{#4} \ssep}
\newcommand{\inp}[4]{\sfromto{#1}{#2}{#3} \inpses \boundv{#4} \ssep}
\newcommand{\del}[5]{\sfromto{#1}{#2}{#3} \outses \freev{\srole{#4}{#5}} \ssep}
\newcommand{\sel}[4]{\sfromto{#1}{#2}{#3} \selses #4 \ssep}
\newcommand{\bra}[4]{\sfromto{#1}{#2}{#3} \brases \set{#4}}
\newcommand{\bras}[4]{\sfromto{#1}{#2}{#3} \brases #4}
\newcommand{\braP}[3]{\sfromto{#1}{#2}{#3} \brases \lPi}

% Arrive construct
\newcommand{\arrivetext}{\mathtt{arrive}}
\newcommand{\arrive}[1]{\arrivetext\ #1}
\newcommand{\arrivem}[2]{\arrivetext\ #1\ #2}

% Typecase construct
\newcommand{\typecasetext}{\mathtt{typecase}}
\newcommand{\oftext}{\mathtt{of}}
\newcommand{\typecase}[2]{\typecasetext\ #1\ \oftext\ \set{#2}}

% IO symbols
\newcommand{\inputsym}{\mathtt{i}}
\newcommand{\outputsym}{\mathtt{o}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                      SUBJECT REDUCTION
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% typing reduction
\newcommand{\typingred}{\red}
\newcommand{\typingRed}{\Red}

\newcommand{\wellconf}[1]{\mathtt{wc}(#1)}
\newcommand{\cohses}[2]{\mathtt{co}(#1(#2))}
\newcommand{\coherent}[1]{\mathtt{co}(#1)}
\newcommand{\fcoherent}[1]{\mathtt{fco}(#1)}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                      SESSION ENDPOINTS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Asynchronous syntax
%\newcommand{\mareq}[4]{\newsp{\srole{#2}{#3}, \dots, \srole{#2}{#4}}{\send{#1}[#3] \freev{#2} \Par \dots \Par \send{#1}[#4]\freev{#2}}}

%\newcommand{\areqs}[3]{\send{#1}[\set{#2}] \freev{#3}}

% Queues
\newcommand{\emp}{\epsilon}
\newcommand{\squeue}[3]{\srole{#1}{#2}:#3}
\newcommand{\srqueue}[4]{\srole{#1}{#2}[\inputsym: #3, \outputsym: #4]}
\newcommand{\srqueuei}[3]{\srole{#1}{#2}[\inputsym: #3]}
\newcommand{\srqueueo}[3]{\srole{#1}{#2}[\outputsym: #3]}
\newcommand{\srqueueio}[4]{\srole{#1}{#2}[\inputsym: #3, \outputsym: #4]}
\newcommand{\sgqueue}[2]{\srole{#1}:#2}

% Shared Names Queues
\newcommand{\shqueue}[2]{#1[#2]}
%\newcommand{\shqueuet}[3]{#1[#2, #3]}

% IO Queues
\newcommand{\squeueio}[3]{#1[\inputsym: #2, \outputsym: #3]}
\newcommand{\squeuei}[2]{#1[\inputsym: #2]}
\newcommand{\squeueo}[2]{#1[\outputsym: #2]}

\newcommand{\squeuetio}[4]{#1[#2, \inputsym: #3, \outputsym: #4]}
\newcommand{\squeueto}[3]{#1[#2, \outputsym: #3]}
\newcommand{\squeueti}[3]{#1[#2, \inputsym: #3]}
\newcommand{\squeuet}[2]{#1[#2]}

% Queue Values

\newcommand{\queuev}[2]{\role{#1}(#2)}
\newcommand{\queuel}[2]{\role{#1} #2}
\newcommand{\queues}[3]{\role{#1}(\srole{#2}{#3})}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                        GLOBAL SESSION TYPES
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\impl}[2]{\{\!\{#1\}\!\}_{\mathcal{#2}}}
\newcommand{\impll}[2]{\{\!\{#1\}\!\}_{\mathcal{#2}}^\fw}

\newcommand{\gtfont}[1]{\mathtt{#1}}
\newcommand{\gsep}{.}

\newcommand{\globaltype}[1]{\lrangle{#1}}
\newcommand{\parties}[1]{\mathtt{\pa}(#1)}
\newcommand{\roles}[1]{\mathtt{roles}(#1)}

\newcommand{\fromtogt}[2]{#1 \rightarrow #2 \semicolon}

\newcommand{\valuegt}[3]{\fromtogt{#1}{#2} \lrangle{#3} \gsep}
\newcommand{\selgt}[3]{\fromtogt{#1}{#2} \set{#3}}
\newcommand{\selgtG}[2]{\fromtogt{#1}{#2} \lGi}
\newcommand{\recgt}[2]{\mu \vart{#1}. #2}
\newcommand{\vargt}[1]{\vart{#1}}
\newcommand{\inactgt}{\gtfont{end}}

\newcommand{\swap}{\ensuremath{\approx_{\mathtt{sw}}}\xspace}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                              GLOBAL SESSION TYPES EQUIVALENCE
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\projset}[1]{\mathtt{proj}(#1)}
\newcommand{\aprojset}[1]{\mathtt{aproj}\ #1 }
\newcommand{\gcong}{\equiv}
\newcommand{\govcong}{\cong_g}
\newcommand{\gperm}{\simeq}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                        PROJECTION
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\projsymb}{\lceil}
\newcommand{\proj}[2]{#1 \projsymb #2}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                        LOCAL SESSION TYPES
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\tfont}[1]{\mathtt{#1}}
\newcommand{\tsep}{;}

\newcommand{\chtype}[1]{\lrangle{#1}}
\newcommand{\chtypei}[1]{\inputsym \lrangle{#1}}
\newcommand{\chtypeo}[1]{\outputsym \lrangle{#1}}
\newcommand{\chtypeio}[1]{\inputsym \outputsym \lrangle{#1}}

\newcommand{\outtype}{\outses}
\newcommand{\inptype}{\inpses}
\newcommand{\seltype}{\selses}
\newcommand{\bratype}{\brases}

\newcommand{\trec}[2]{\mu\vart{#1}.#2}
\newcommand{\tvar}[1]{\vart{#1}}
%\newcommand{\settype}[1]{\set{#1}}
\newcommand{\tset}[1]{\set{#1}}
\newcommand{\tinact}{\tfont{end}}

%\newcommand{\sminus}[1]{#1^-}
\newcommand{\sminus}[1]{#1^{\text{--}}}

\newcommand{\subt}{\leq}
\newcommand{\supt}{\geq}

% Multiparty Local Session Types
\newcommand{\tout}[2]{\role{#1} \outtype \lrangle{#2} \tsep}
\newcommand{\tinp}[2]{\role{#1} \inptype (#2) \tsep}
\newcommand{\tsel}[2]{\role{#1} \seltype \set{#2}}
\newcommand{\tsels}[2]{\role{#1} \seltype #2}
\newcommand{\tselT}[1]{\role{#1} \seltype \lTi}
\newcommand{\tbra}[2]{\role{#1} \bratype \set{#2}}
\newcommand{\tbras}[2]{\role{#1} \bratype #2}
\newcommand{\tbraT}[1]{\role{#1} \bratype \lTi}

% Binary Session Types
\newcommand{\btout}[1]{\outtype \lrangle{#1} \tsep}
\newcommand{\bbtout}[1]{\outtype \big\langle{#1}\big\rangle \tsep}
\newcommand{\btinp}[1]{\inptype (#1) \tsep}
\newcommand{\bbtinp}[1]{\inptype \big({#1}\big) \tsep}
\newcommand{\btsel}[1]{\oplus \set{#1}}
\newcommand{\btselS}{\oplus \lSi}
\newcommand{\btbra}[1]{\& \set{#1}}
\newcommand{\btbraS}{\& \lSi}

% Queue Typing

\newcommand{\mtout}[2]{\role{#1} \outtype \lrangle{#2}}
\newcommand{\mtinp}[2]{\role{#1} \inptype (#2)}
\newcommand{\mtsel}[2]{\role{#1} \seltype #2}
\newcommand{\mtbra}[2]{\role{#1} \bratype #2}


% Binary Queue Typing

\newcommand{\bmtout}[1]{\outtype \lrangle{#1}}
\newcommand{\bmtinp}[1]{\inptype (#1)}
\newcommand{\bmtsel}[1]{\seltype #1}
\newcommand{\bmtbra}[1]{\bratype #1}

% Message concatanation
\newcommand{\mcat}{\;*\;}
\newcommand{\icat}{\;\circ\;}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                        TYPED PROCESSES
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\Ga}{\Gamma}
\newcommand{\De}{\Delta}
\newcommand{\proves}{\vdash}
\newcommand{\hastype}{\triangleright}

\newcommand{\Decat}[1]{\De \cat #1}
\newcommand{\Gacat}[1]{\Ga \cat #1}

\newcommand{\tcat}{\circ}

\newcommand{\typed}[1]{#1:}
\newcommand{\typedrole}[2]{\typed{\srole{#1}{#2}}}
%\newcommand{\typedqrole}[2]{\typed{\srole{#1^{[]}}{#2}}}

\newcommand{\typedprocess}[3]{#1 \proves #2 \hastype #3}

\newcommand{\Eproves}[3]{#1 \proves \typed{#2} #3}
\newcommand{\Gproves}[2]{\Eproves{\Ga}{#1}{#2}}

\newcommand{\tprocess}[3]{#1 \proves #2 \hastype #3}
\newcommand{\Gtprocess}[2]{\tprocess{\Ga}{#1}{#2}}
\newcommand{\Gptprocess}[2]{\tprocess{\Ga'}{#1}{#2}}

\newcommand{\noGtprocess}[2]{#1 \hastype #2}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                    MULTIPARTY TYPED THEORY
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\globalenv}[1]{\set{#1}}
%\newcommand{\globalenvI}{\set{\typed{s_i} \G_i}_{i \in I}}
\newcommand{\globalenvI}{E}
\newcommand{\globalenvJ}{\set{\typed{s_j} \G_j}_{j \in J}}

\newcommand{\Gltprocess}[4]{\tprocess{#1}{#2}{#3, #4}}

\newcommand{\geI}{\globalenvI}
\newcommand{\geJ}{\globalenvJ}

\newcommand{\Stprocess}[3]{\tprocess{\geI, #1}{#2}{#3}}
\newcommand{\SGtprocess}[2]{\Gtprocess{#1}{#2, \globalenvI}}
\newcommand{\SJGtprocess}[2]{\globalenvJ, \Gtprocess{#1}{#2}}

\newcommand{\Observer}[2]{\mathsf{Observer}(#1, #2)}
\newcommand{\ObserverG}[1]{\mathsf{Observer}(\globalenvI, #1)}

\newcommand{\Obs}{\ensuremath{\mathsf{Obs}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                        BEHAVIOURAL THEORY
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\fromtolts}[2]{\fromto{#1}{#2}}

\newcommand{\outlts}{\outses}
\newcommand{\inplts}{\inpses}
\newcommand{\sellts}{\oplus}
\newcommand{\bralts}{\&}

% Multiparty Labels
\newcommand{\actreq}[3]{\send{#1} \role{#2} \boundv{#3}}
%\newcommand{\actbreq}[3]{\send{#1} \role{#2} \boundv{#3}}

\newcommand{\actreqs}[3]{\send{#1} \role{\set{#2}} \boundv{#3}}
%\newcommand{\actbreqs}[3]{\send{#1} \role{\set{#2}} \boundv{#3}}

\newcommand{\actacc}[3]{#1 \role{#2} \boundv{#3}}
\newcommand{\actaccs}[3]{#1 \role{\set{#2}} \boundv{#3}}

\newcommand{\actout}[4]{#1 \fromtolts{#2}{#3} \outlts \freev{#4}}
\newcommand{\actqout}[4]{#1^{[]} \fromtolts{#2}{#3} \outlts \freev{#4}}
\newcommand{\actbout}[4]{#1 \fromtolts{#2}{#3} \outlts \boundv{#4}}

\newcommand{\actdel}[5]{#1 \fromtolts{#2}{#3} \outlts \freev{\srole{#4}{#5}}}
\newcommand{\actbdel}[5]{#1 \fromtolts{#2}{#3} \outlts \boundv{\srole{#4}{#5}}}
\newcommand{\actqdel}[5]{#1^{[]} \fromtolts{#2}{#3} \outlts \boundv{\srole{#4}{#5}}}

\newcommand{\actinp}[4]{#1 \fromtolts{#2}{#3} \inplts \freev{#4}}
\newcommand{\actqinp}[4]{#1^{[]} \fromtolts{#2}{#3} \inplts \freev{#4}}

\newcommand{\actsel}[4]{#1 \fromtolts{#2}{#3} \sellts #4}
\newcommand{\actqsel}[4]{#1^{[]} \fromtolts{#2}{#3} \sellts #4}

\newcommand{\actbra}[4]{#1 \fromtolts{#2}{#3} \bralts #4}
\newcommand{\actqbra}[4]{#1^{[]} \fromtolts{#2}{#3} \bralts #4}

\newcommand{\actval}[4]{#1: #2 \rightarrow #3:#4}
\newcommand{\actgsel}[4]{#1: #2 \rightarrow #3:#4}

% Binary Labels
\newcommand{\bactreq}[2]{\send{#1} \freev{#2}}
\newcommand{\bactbreq}[2]{\send{#1} \boundv{#2}}
\newcommand{\bactacc}[2]{#1 \freev{#2}}

\newcommand{\bactout}[2]{#1 \outlts \freev{#2}}
\newcommand{\bactbout}[2]{#1\outlts \boundv{#2}}
\newcommand{\bactinp}[2]{#1 \inplts \freev{#2}}
\newcommand{\bactsel}[2]{#1 \sellts #2}
\newcommand{\bactbra}[2]{#1 \bralts #2}

% Labelled transition relations
\newcommand{\by}[1]{\stackrel{#1}{\longrightarrow}}
\newcommand{\By}[1]{\stackrel{#1}{\Longrightarrow}}

\newcommand{\hby}[1]{\stackrel{#1}{\longmapsto}}
\newcommand{\Hby}[1]{\stackrel{#1}{\Longmapsto}}


% Session barbs
\newcommand{\barbreq}[1]{\barb{#1}}
%\newcommand{\barbacc}[2]{\barb{#1\role{\set{#2}}}}
\newcommand{\barbout}[3]{\barb{\sfromto{#1}{#2}{#3}}}
%\newcommand{\barbinp}[3]{\barb{#1\fromto{#2}{#3}\inpses}}

\newcommand{\Barbreq}[2]{\Barb{\send{#1}\role{#2}}}
%\newcommand{\Barbacc}[2]{\Barb{#1\role{\set{#2}}}}
%\newcommand{\Barbout}[3]{\Barb{\sfromto{#1}{#2}{#3}\outses}}
\newcommand{\Barbout}[3]{\Barb{\sfromto{#1}{#2}{#3}}}
%\newcommand{\Barbinp}[3]{\Barb{#1\fromto{#2}{#3}\inpses}}

% Binary Session barbs
\newcommand{\bbarbreq}[1]{\barb{#1}}
%\newcommand{\bbarbacc}[1]{\barb{#1}}
\newcommand{\bbarbout}[1]{\barb{#1}}
%\newcommand{\bbarbinp}[1]{\barb{#1\inpses}}

\newcommand{\bBarbreq}[1]{\Barb{\send{#1}}}
%\newcommand{\bBarbacc}[2]{\Barb{#1}}
\newcommand{\bBarbout}[1]{\Barb{#1\outses}}
%\newcommand{\bBarbinp}[1]{\Barb{#1\inpses}}

\newcommand{\comp}{\asymp}
\newcommand{\coh}{\asymp}
\newcommand{\bistyp}{\rightleftharpoons}

\newcommand{\typingbeh}{\leftrightarrow}

\newcommand{\bufrel}{\succ}

\newcommand{\ordercup}{\bowtie}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                TYPED TRANSITIONS - REDUCTIONS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Environment Transitions
\newcommand{\envtrans}[1]{\by{#1}}
\newcommand{\envTrans}[1]{\by{#1}}
\newcommand{\typedtrans}[1]{\by{#1}}
\newcommand{\typedTrans}[1]{\By{#1}}
\newcommand{\typedred}{\red}
\newcommand{\typedRed}{\Red}

% Typed Environment Transitions - Binary case
\newcommand{\benv}[2]{(#1, #2)}
\newcommand{\bGenv}[1]{\benv{\Ga}{#1}}
\newcommand{\bGDenv}{\envtyp{\Ga}{\De}}

\newcommand{\envby}[5]{\benv{#1}{#2} \envtrans{#3} \benv{#4}{#5}}
\newcommand{\Genvby}[3]{\envby{\Ga}{#1}{#2}{\Ga}{#3}}

% Typed Environment Transitions - Multiparty case

\newcommand{\env}[3]{(#1, #2, #3)}
\newcommand{\Genv}[2]{\env{\globalenvI}{#1}{#2}}
\newcommand{\GGenv}[1]{\env{\globalenvI}{\Ga}{#1}}
\newcommand{\GGDenv}{\env{\globalenvI}{\Ga}{\De}}

% Typed Process Transitions - Binary case

\newcommand{\ftby}[7]{\tprocess{#1}{#2}{#3} \typedtrans{#4} \tprocess{#5}{#6}{#7}}
\newcommand{\ftBy}[7]{\tprocess{#1}{#2}{#3} \typedTrans{#4} \tprocess{#5}{#6}{#7}}

\newcommand{\tpby}[6]{\tprocess{#1}{#2}{#3} \typedtrans{#4} \noGtprocess{#5}{#6}}
\newcommand{\tpBy}[6]{\tprocess{#1}{#2}{#3} \typedTrans{#4} \noGtprocess{#5}{#6}}
\newcommand{\Gtpby}[5]{\Gtprocess{#1}{#2} \typedtrans{#3} \noGtprocess{#4}{#5}}
\newcommand{\GtpBy}[5]{\Gtprocess{#1}{#2} \typedTrans{#3} \noGtprocess{#4}{#5}}

\newcommand{\GGtpby}[5]{\tprocess{\globalenvI, \Ga}{#1}{#2} \typedtrans{#3} \noGtprocess{#4}{#5}}
\newcommand{\GGtpBy}[5]{\tprocess{\globalenvI, \Ga}{#1}{#2} \typedTrans{#3} \noGtprocess{#4}{#5}}

% Typed Reductions - Binary case

\newcommand{\ftpred}[6]{\tprocess{#1}{#2}{#3} \typedred \tprocess{#4}{#5}{#6}}
\newcommand{\ftpRed}[6]{\tprocess{#1}{#2}{#3} \typedRed \tprocess{#4}{#5}{#6}}

\newcommand{\tpred}[5]{\tprocess{#1}{#2}{#3} \typedred \noGtprocess{#4}{#5}}
\newcommand{\tpRed}[5]{\tprocess{#1}{#2}{#3} \typedRed \noGtprocess{#4}{#5}}
\newcommand{\Gtpred}[4]{\Gtprocess{#1}{#2} \typedred \noGtprocess{#3}{#4}}
\newcommand{\GtpRed}[4]{\Gtprocess{#1}{#2} \typedRed \noGtprocess{#3}{#4}}

% Observer Reductions

\newcommand{\obsred}{\red_{obs}}
\newcommand{\obsRed}{\Red_{obs}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                    TYPED RELATIONS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Typed Relations
\newcommand{\fulltrel}[7]{\rel{\typedprocess{#1}{#2}{#3}}{#4}{\typedprocess{#5}{#6}{#7}}}
\newcommand{\treld}[6]{\rel{\typedprocess{#1}{#2}{#3}}{#4}{\noGtypedprocess{#5}{#6}}}
\newcommand{\trel}[5]{\rel{#1 \proves #2}{#3}{\noGtypedprocess{#4}{#5}}}

\newcommand{\tcong}{\cong}
\newcommand{\twb}{\approx}
\newcommand{\govwb}{\approx_g}
\newcommand{\tequiv}{\approx}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                    CONFIGURATION THEORY
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\confpair}[2]{(#1, #2)}
\newcommand{\uptoconfpair}[2]{[#1, #2]}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                   CONFLUENCE DETERMINACY
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\sesstrans}[1]{\stackrel{#1}{\longrightarrow_{s}}}
\newcommand{\sessTrans}[1]{\stackrel{#1}{\Longrightarrow_{s}}}

\newcommand{\fulltypedsesstrans}[7]{\typedprocess{#1}{#2}{#3} \sesstrans{#4} \typedprocess{#5}{#6}{#7}}
\newcommand{\fulltypedsessTrans}[7]{\typedprocess{#1}{#2}{#3} \sessTrans{#4} \typedprocess{#5}{#6}{#7}}

\newcommand{\typedsesstrans}[6]{\typedprocess{#1}{#2}{#3} \sesstrans{#4} \noGtypedprocess{#5}{#6}}
\newcommand{\typedsessTrans}[6]{\typedprocess{#1}{#2}{#3} \sessTrans{#4} \noGtypedprocess{#5}{#6}}
\newcommand{\Gtypedsesstrans}[5]{\Gtypedprocess{#1}{#2} \sesstrans{#3} \noGtypedprocess{#4}{#5}}
\newcommand{\GtypedsessTrans}[5]{\Gtypedprocess{#1}{#2} \sessTrans{#3} \noGtypedprocess{#4}{#5}}

% Actions
\newcommand{\confact}[2]{#1 \lfloor #2}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                    MAPPING AND ENCODINGS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\map}[1]{[\!\![#1]\!\!]}
\newcommand{\umap}[1]{[\!\![#1]\!\!]^u}
\newcommand{\pmap}[2]{\ensuremath{[\!\![#1]\!\!]^#2}}
\newcommand{\pmapp}[3]{\ensuremath{[\!\![#1]\!\!]^#2_#3}}
\newcommand{\auxmap}[2]{\ensuremath{\{\!\{#1\}\!\}^#2}}
\newcommand{\tauxmap}[2]{\ensuremath{\{\!|#1|\!\}^#2}}
\newcommand{\auxmapp}[3]{\ensuremath{\big\lfloor\!\!\big\lfloor#1\big\rfloor\!\!\big\rfloor^#2_#3}}
\newcommand{\tmap}[2]{\ensuremath{(\!\!\langle#1\rangle\!\!)^{#2}}}
\newcommand{\vtmap}[2]{{\ensuremath{\big\lfloor #1\big\rfloor^{#2}}}}
\newcommand{\mapt}[1]{\ensuremath{(\!\!\langle#1\rangle\!\!)}}
\newcommand{\mapa}[1]{\ensuremath{\{\!\!\{#1\}\!\!\}}}
\newcommand{\namemap}[2]{#1\map{#2}}

\newcommand{\enc}[2]{\big\langle\map{#1}, \mapt{#2}\big\rangle}
\newcommand{\enco}[1]{\big\langle #1\big\rangle}
\newcommand{\encod}[3]{\lrangle{\map{#1}^{#3}, \mapt{#2}^{#3}}}
\newcommand{\fencod}[4]{\lrangle{\map{#1}^{#3}_{#4} \, , \, \mapt{#2}^{#3}}}

\newcommand{\calc}[5]{\lrangle{#1, #2, #3, #4, #5}}
\newcommand{\tyl}[1]{\ensuremath{\mathcal{#1}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                    PI CONSTRUCTS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\constrtype}[1]{\mathtt{#1}}


\newcommand{\Let}{\constrtype{let}\ }
\newcommand{\In}{\constrtype{in}\ }
\newcommand{\To}{\constrtype{to}\ }
\newcommand{\new}{\constrtype{new}\ }
\newcommand{\from}{\constrtype{from}\ }
\newcommand{\select}{\constrtype{select}\ }
\newcommand{\register}{\constrtype{register}\ }
\newcommand{\Update}{\constrtype{update}\ }

\newcommand{\selectfrom}[2]{\select #1\ \from #2\ \In}
\newcommand{\registerto}[2]{\register #1\ \To #2\ \In}

\newcommand{\newselector}[1]{\new \constrtype{sel}\ #1\ \In}
\newcommand{\newselectorT}[2]{\new \constrtype{sel}\lrangle{#2}\ #1\ \In}
\newcommand{\selecttype}[1]{\dual{\constrtype{sel}}\lrangle{#1}}
\newcommand{\sselecttype}[1]{\constrtype{sel}\lrangle{#1}}

\newcommand{\update}[3]{\Update(#1, #2, #3)\ \In}

\newcommand{\newenv}[1]{\new \mathtt{env}\ #1\ \In\ }
\newcommand{\Letin}[2]{\Let #1 = #2\ \In}

\newcommand{\selqueue}[2]{#1\lrangle{#2}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                    DUALITY
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\dualof}{\ \mathsf{dual}\ }


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                        lambda - CALCULUS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\labs}[2]{\lambda #1. #2}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                    HIGHER ORDER SESSION PI
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\newcommand{\pHOp}{\ensuremath{\mathsf{HO}\pi_{\mathsf{p}}}\xspace}
%\newcommand{\pHOpnr}{\ensuremath{\mathsf{HO}\pi^{-\mu}_{\mathsf{p}}}\xspace}
\newcommand{\HOp}{\ensuremath{\mathsf{HO}\pi}\xspace}
%\newcommand{\sessp}{\ensuremath{\mathtt{SE}\pi}\xspace}
\newcommand{\sessp}{\ensuremath{\pi}\xspace}
\newcommand{\haskp}{\ensuremath{\pi^{\lambda}}\xspace}
\newcommand{\pHOp}{\ensuremath{\mathsf{HO}\tilde{\pi}}\xspace}
%\newcommand{\psesp}{\ensuremath{\mathtt{sess}\pi_{\mathsf{p}}}\xspace}
%\newcommand{\psespnr}{\ensuremath{\mathtt{sess}\pi^{-\mu}_{\mathsf{p}}}\xspace}
%\newcommand{\sespnr}{\ensuremath{\mathtt{sess}\pi^{-\mu}}\xspace}
\newcommand{\HO}{\ensuremath{\mathsf{HO}}\xspace}
\newcommand{\HOpp}{\ensuremath{\mathsf{HO\pi^{+}}}\xspace}
\newcommand{\PHOp}{\ensuremath{\mathsf{HO}\,{\widetilde{\pi}}}\xspace}
\newcommand{\PHOpp}{\ensuremath{\mathsf{HO}\,{\widetilde{\pi}}^{\,+}}\xspace}
\newcommand{\PHO}{\ensuremath{\vec{\mathsf{HO}}}\xspace}
\newcommand{\Psessp}{\ensuremath{\vec{\pi}}\xspace}


\newcommand{\CAL}{\ensuremath{\mathsf{C}}\xspace}

%\newcommand{\pol}{\mathsf{p}}


\newcommand{\ST}{\mathsf{ST}}


%\newcommand{\pHO}{\mathsf{pure\ HO}}

%\newcommand{\HOp}{\HO^+}
%\newcommand{\pHOp}{\pHO^+}
%\newcommand{\ppi}{\mathsf{pure\ session\ }\pi}
%\newcommand{\spi}{\mathsf{session\ }\pi}

\newcommand{\Proc}{\ensuremath{\diamond}}


%\newcommand{\appl}[2]{#1\lrangle{#2}}
\newcommand{\appl}[2]{#1\, {#2}}
%\newcommand{\abs}[2]{(#1)#2}
\newcommand{\abs}[2]{\lambda #1.\,#2}

\newcommand{\lollipop}{\multimap}
\newcommand{\sharedop}{\rightarrow}
\newcommand{\logicop}{\multimapdot}

\newcommand{\lhot}[1]{#1\! \lollipop\! \diamond}
\newcommand{\shot}[1]{#1\! \sharedop\! \diamond}
\newcommand{\thunkt}{\ensuremath\{\!\{\diamond\}\!\}}
\newcommand{\thunkp}[1]{\ensuremath\{\!\{#1\}\!\}}
\newcommand{\dummyn}{\ensuremath{\ast}}
\newcommand{\hot}[1]{#1 \logicop \diamond}

%\newcommand{\absmap}[1]{}
\newcommand{\vmap}[1]{|\!|#1|\!|}
\newcommand{\smap}[1]{(\!|\!|#1|\!|\!)^s}
\newcommand{\svmap}[1]{(\!|\!|#1|\!|\!)^{s\rightarrow v}}
\newcommand{\amap}[1]{\mathcal{A}\map{#1}}
\newcommand{\absmap}[2]{\mathcal{A}\map{#1}^{#2}}



%%%%% triggers

\newcommand{\hotrigger}[2]{\binp{#1}{x} \newsp{s}{\appl{x}{s} \Par \bout{\dual{s}}{#2} \inact}}
\newcommand{\fotrigger}[5]{\binp{#1}{#2} \newsp{#3}{\map{#4}^{#3} \Par \bout{\dual{#3}}{#5} \inact}}
%\newcommand{\fotrigger}[2]{\binp{#1}{X} \appl{X}{#2}}

%%%%%% Typed relations

\newcommand{\horel}[6]{#1; #2 \proves #3 #4 #5 \proves #6}
%\newcommand{\horel}[6]{#1; \es; #2 \proves #3 #4 #5 \proves #6}

\newcommand{\mhorel}[7]{
	\begin{array}{rcll}
		#1; \es; #2 &#4& #5 \proves& #3\\
			&#4& #6 & #7
	\end{array}
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                    LN TRANSFORM
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\Loop}{\mathsf{Loop}}
\newcommand{\CodeBlocks}{\mathsf{CodeBlocks}}

\newcommand{\lnmap}[1]{\namemap{LN}{#1}}
\newcommand{\lnrmap}[1]{\namemap{LNR}{#1}}
\newcommand{\lnblockmap}[1]{\namemap{\mathcal{B}}{#1}}
\newcommand{\lnnonblockmap}[2]{\map{#1, #2}}

\newcommand{\mapenv}[2]{\map{#1}_{#2}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                        GENERAL TYPES
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Values
\newcommand{\true}{\sessionfont{tt}}
\newcommand{\false}{\sessionfont{ff}}

% Typed
\newcommand{\bool}{\sessionfont{bool}}
\newcommand{\nat}{\sessionfont{nat}}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                        PROCESSES NAMES SESSIONS ETC
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Processes
\newcommand{\PP}{\ensuremath{P}}
\newcommand{\Q}{\ensuremath{Q}}
\newcommand{\R}{\ensuremath{R}}
\newcommand{\OP}{\ensuremath{\mathsf{O}}}

% Global environments
\newcommand{\En}{\ensuremath{En}}

% Session channels
\newcommand{\s}{\ensuremath{s}}
\newcommand{\ds}{\ensuremath{\dual{s}}}
%\newcommand{\Ms}[2]{\ensuremath{s}\role{#1}\role{#2}}

%Dummy channels
\newcommand{\sd}{\mathtt{sd}}
\newcommand{\shd}{\mathtt{shd}}

% Names
\newcommand{\Ia}{\ensuremath{a}}
\newcommand{\Iu}{\ensuremath{u}}

% Variables, values, expressions
\newcommand{\x}{\ensuremath{x}}
\newcommand{\y}{\ensuremath{y}}
\newcommand{\ks}{\ensuremath{k}}
\newcommand{\cc}{\ensuremath{c}}
\newcommand{\va}{\ensuremath{v}}
%\newcommand{\e}{\ensuremath{e}}
\newcommand{\n}{\ensuremath{n}}

% Process Variables

\newcommand{\X}{\varp{X}}
\newcommand{\Y}{\varp{Y}}

% Roles
\newcommand{\p}{\ensuremath{\mathtt{p}}\xspace}
\newcommand{\pa}{\ensuremath{\mathtt{pa}}}
\newcommand{\q}{\ensuremath{\mathtt{q}}\xspace}
\newcommand{\er}{\ensuremath{\mathtt{r}}}
\newcommand{\A}{\ensuremath{A}}

% Types
%\newcommand{\G}{\ensuremath{G}}
\newcommand{\gG}{\globaltype{\G}}
%\newcommand{\U}{\ensuremath{U}}
\newcommand{\So}{\ensuremath{S}}
\newcommand{\T}{\ensuremath{T}}

% Queue Types
\newcommand{\M}{\ensuremath{M}}
\newcommand{\I}{\ensuremath{M_\inputsym}}
\newcommand{\Om}{\ensuremath{M_\outputsym}}
\newcommand{\Typ}{\ensuremath{\mathsf{T}}}

% Queues values
\newcommand{\h}{\ensuremath{h}}

%barbs
\newcommand{\m}{\ensuremath{\mu}}

% Contexts
%\newcommand{\C}{\ensuremath{{\mathbb{C}}}}
\newcommand{\E}{\ensuremath{E}}

% Congruence completness - Definibility
\newcommand{\TT}{\ensuremath{T}}
\newcommand{\suc}{\textrm{succ}}
\newcommand{\fail}{\textrm{fail}}


% Set selection labels
\newcommand{\lPi}{\set{l_i:\PP_i}_{i \in I}}
\newcommand{\lGi}{\set{l_i:\G_i}_{i \in I}}
\newcommand{\lTi}{\set{l_i:\T_i}_{i \in I}}
\newcommand{\lSi}{\set{l_i:\So_i}_{i \in I}}

% Selector proof

\newcommand{\SEL}{P_\mathit{Sel}}
\newcommand{\DSEL}{P_\mathit{DSel}}
\newcommand{\Sel}{\mathsf{Sel}}
\newcommand{\IfSel}{\mathsf{IfSel}}
\newcommand{\DSel}{\mathsf{DSel}}
\newcommand{\PSel}{\mathsf{PermSel}}
\newcommand{\PIfSel}{\mathsf{PermIfSel}}
\newcommand{\PDSel}{\mathsf{PermDSel}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                        ENVIRONMENTS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\newtheorem{fact}{Fact}[section]
\newtheorem{notation}{Notation}
%\newtheorem{remark}{Remark}

%\newenvironment{notation}{\paragraph{{\bf Notation}}}{}

%\newtheorem{proposition}[fact]{{\bf\em Proposition}}
%\newtheorem{example}[fact]{{\bf\em Example}}
%\newtheorem{lemma}[fact]{{\bf\em Lemma}}
%\newtheorem{corollary}[fact]{{\bf\em Corollary}}
%\newtheorem{definition}[fact]{{\bf\em Definition}}
%\newtheorem{theorem}[fact]{{\bf\em Theorem}}
%\newtheorem{remark}[fact]{{\bf\em Remark}}

\newcommand{\nonhosyntax}[1]{\colorbox{lightgray}{\ensuremath{#1}}}
\newcommand{\nonpisyntax}[1]{\fcolorbox{black}{white}{\ensuremath{#1}}}
\newcommand{\rtsyn}[1]{\fcolorbox{black}{white}{\ensuremath{#1}}}

\newenvironment{mytheorem}{%\vspace{-3pt}
	\begin{theorem}
}{%\vspace{-4pt}
	\end{theorem}
}

\newenvironment{myproposition}{
	\begin{proposition}%\vspace{-3pt}
}{%\vspace{-4pt}
	\end{proposition}
}

\newenvironment{mycorollary}{
	\begin{corollary}%\vspace{-3pt}
}{%\vspace{-4pt}
	\end{corollary}
}

\newenvironment{mylemma}{
	\begin{lemma}%\vspace{-3pt}
}{%\vspace{-4pt}
	\end{lemma}
}


\newenvironment{mydefinition}{%\vspace{-3pt}
	\begin{definition}
}{%\vspace{-3pt}
	\end{definition}
}

%\newenvironment{proof}{
%	{\em Proof.}
%}{}


%\newcommand{\qed}{\ensuremath{\square}}





%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                        MISC
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\Appendix}[1]{Appendix \ref{#1}}

\newcommand{\dimcom}[1]{{\bf Comment: #1 \\}}

\newcommand{\hintcom}[1]{{\bf Hint: #1 \\}}

\newif\ifny\nyfalse
%\nytrue
\newcommand{\NY}[1]
{\ifny{\color{purple}{#1}}\else{#1}\fi}

\newcommand{\KH}[1]
{\ifny{\color{brown}{#1}}\else{#1}\fi}

\newif\ifdm\dmtrue
%\dmfalse
\newcommand{\dk}[1]
{\ifdm{\color{blue}{#1}}\else{#1}\fi}

\newif\ifrhu\rhutrue
%\rhufalse
\newcommand{\rh}[1]
{\ifdm{\color{red}{#1}}\else{#1}\fi}

\newif\ifjp\jptrue
%\jpfalse
%\newcommand{\jp}[1]
%{\ifjp{\color{red}{#1}}\else{#1}\fi}

\newif\ifjp\jptrue
\jpfalse
\newcommand{\jpc}[1]
{\ifjp{\color{red}{#1}}\else{#1}\fi}


%\newcommand{\newj}[1]{\textcolor{red}{#1}}
\newcommand{\newj}[1]{{#1}}
%\newcommand{\newjb}[1]{\textcolor{blue}{#1}}
\newcommand{\newjb}[1]{{#1}}

\newcommand{\ENCan}[1]{\langle #1 \rangle}
\newcommand{\NI}{\noindent}


\newcommand{\syntaxvspace}{\\[1mm]}

\newcommand{\TO}[2]{#1\to #2}
\newcommand{\GS}[3]{\TO{#1}{#2}\colon \!\ENCan{#3}}

\newcommand{\ASET}[1]{\{#1\}}
\newcommand{\participant}[1]{\mathtt{#1}}
\newcommand{\CODE}[1]{{\tt #1}}

\newcommand{\AT}[2]{#1 \! : \! #2}


\newcommand{\myrm}{}


\newcommand{\secref}[1]{\S\,\ref{#1}}
\newcommand{\defref}[1]{Def.~\ref{#1}}
\newcommand{\notref}[1]{Not.~\ref{#1}}
\newcommand{\defsref}[1]{Defs.~\ref{#1}}
\newcommand{\figref}[1]{Fig.~\ref{#1}}
\newcommand{\thmref}[1]{Thm.~\ref{#1}}
\newcommand{\thmsref}[1]{Thms.~\ref{#1}}
\newcommand{\exref}[1]{Ex.~\ref{#1}}
\newcommand{\propref}[1]{Prop.~\ref{#1}}
\newcommand{\propsref}[1]{Props.~\ref{#1}}
\newcommand{\appref}[1]{App.~\ref{#1}}
\newcommand{\lemref}[1]{Lem.~\ref{#1}}



\newcommand{\stytra}[6]{\ensuremath{#1; #3 \proves #4 \hby{#2} #5 \proves #6 }}
\newcommand{\stytraarg}[7]{\ensuremath{#1; #3 \proves_{#7} #4 \hby{#2} #5 \proves_{#7} #6 }}
\newcommand{\stytraargi}[8]{\ensuremath{#1; #3 \proves_{#7} #4 \hby{#2}_{#8} #5 \proves_{#7} #6 }}
\newcommand{\wtytra}[6]{\ensuremath{#1; #3 \proves #4 \Hby{#2}  #5 \proves #6}}
\newcommand{\wtytraarg}[7]{\ensuremath{#1; #3 \proves_{#7} #4 \Hby{#2}  #5 \proves_{#7} #6 }}
\newcommand{\wtytraargi}[8]{\ensuremath{#1; #3 \proves_{#7} #4 \Hby{#2}_{#8}  #5 \proves_{#7} #6 }}
\newcommand{\wbb}[6]{\ensuremath{#1; #3 \proves #4 \wb #5 \proves #6 }}
\newcommand{\wbbarg}[7]{\ensuremath{#1; #3 \proves_{#7} #4 \wb_{#7} #5 \proves_{#7} #6 }}

\newcommand{\minussh}{\ensuremath{\mathsf{-sh}}\xspace}

\definecolor{lightgray}{gray}{0.75}

\newcommand\greybox[1]{%
  \vskip\baselineskip%
  \par\noindent\colorbox{lightgray}{%
    \begin{minipage}{\textwidth}#1\end{minipage}%
  }%
  \vskip\baselineskip%
}

%\newcommand{\myparagraph}[1]{\paragraph{\bf #1}}

\newcommand{\mapchar}[2]{\ensuremath{[\!\!(#1)\!\!]^{#2}}}
\newcommand{\omapchar}[1]{\ensuremath{[\!\!(#1)\!\!]_{\mathsf{c}}}}

\newcommand{\trigger}[3]{#1 \leftarrow\!\!\!\!\!\!\!\leftarrow #2:#3 }
%\newcommand{\htrigger}[2]{#1 \Leftarrow #2}
\newcommand{\ftrigger}[3]{#1 \Leftarrow \AT{#2}{#3}}
\newcommand{\htrigger}[2]{#1 \hookleftarrow #2}

\newcommand{\btau}{\tau_{\beta}}
\newcommand{\stau}{\tau_{s}}
\newcommand{\dtau}{\tau_{d}}



%\newcommand{\HOpp}{\ensuremath{\mathsf{HO\pi^{+}}}\xspace}
%\newcommand{\PHOp}{\ensuremath{\mathsf{HO}{\vec{\pi}}}\xspace}
%\newcommand{\PHOpp}{\ensuremath{\mathsf{HO}{\vec{\pi}}^{+}}\xspace}

%%CLAUDIO MACROS%%
\newcommand{\procs}{\mathcal{P}}
\newcommand{\confs}{\mathcal{M}}
\newcommand{\agents}{\mathcal{A}}
%\newcommand{\keyword}[1]{\mathtt{#1}}
\newcommand{\newg}[1]{\keyword{new }\,(#1)}
\newcommand{\cm}[1]{\textcolor{blue}{[CM: #1]}}
\newcommand{\jp}[1]{\textcolor{red}{[JP: #1]}}
%\newcommand{\added}[1]{\textcolor{orange}{#1}}
\newcommand{\added}[1]{#1}

%%Reversible%%
\newcommand{\fwcolor}[1]{\textcolor{blue}{#1}}
\newcommand{\bkcolor}[1]{\textcolor{red}{#1}}

\newcommand{\rmark}{\blacklozenge}
\newcommand{\normark}{\lozenge}
\newcommand{\hnormark}{\bkcolor{\circ}}


\newcommand{\key}[2]{#1[#2]}
\newcommand{\np}[2]{#1:#2}
\newcommand{\ep}[2]{#1[#2]}
\newcommand{\mysepp}{\cdot}
\newcommand{\mysep}{\,,\,}
\newcommand{\store}{\sigma}
\newcommand{\queue}[1]{\left\lfloor #1 \right\rfloor}
\newcommand{\mytagg}{\spadesuit}
\newcommand{\monig}[4]{\ensuremath{{#1\queue{\textcolor{black}{#2}\mysepp #3\mysepp #4}^{\mytagg}}}}
\newcommand{\moni}[4]{\ensuremath{{#1\queue{\textcolor{black}{#2}\mysepp #3\mysepp #4}}}}
\newcommand{\hmoni}[4]{\ensuremath{{#1\queue{\textcolor{black}{#2}\mysepp #3\mysepp #4}^{\normark}}}}
\newcommand{\monir}[4]{\ensuremath{{#1\queue{\textcolor{black}{#2}\mysepp #3\mysepp #4}^{\bkcolor{\rmark}}}}}
%\newcommand{\moni}[5]{\ensuremath{#1\queue{#2\mysepp #3\mysepp #4\mysepp #5}}}
\newcommand{\mem}[3]{\ensuremath{#1\queue{#2\mysep #3}}}
\newcommand{\past}{\,\textcolor{magenta}{\text{\textbf{\textasciicircum\!\!\textasciicircum}}}}
%\newcommand{\past}{\,\textcolor{magenta}{\ensuremath{ ^\blacktriangle}}\,}
%\newcommand{\past}{\,\textcolor{magenta}{\ensuremath{ ^\curlywedge}}\,}
\newcommand{\typeOut}[2]{#1\outtype \langle #2\rangle}
\newcommand{\typeIn}[2]{#1\inptype ( #2)}

%\newcommand{\coda}[3]{#1:(#2\,:\,#3)}
\newcommand{\coda}[2]{#1:#2}
\newcommand{\history}{\textcolor{magenta}{\mathbf{\star}}}
\newcommand{\codah}[4]{\coda{#1}{(#2\,\history\,#3)\!#4}}
\newcommand{\len}{\mathtt{len}}
\newcommand{\anyv}{m}
\newcommand{\equivq}{\equiv_\mathsf{q}}
%\newcommand{\cons}{::}

\newcommand{\cons}{\circ}
\newcommand{\consh}{\circledwedge}
\newcommand{\valueq}[3]{(#1 \,,\, #2 \,,\,#3)}
\newcommand{\myeval}[2]{#2(#1)}
\newcommand{\ctx}[1]{\mathbb{#1}}
\newcommand{\myctx}[2]{\ctx{#1}[#2]}
\newcommand{\myctxb}[2]{{#1\left[\textcolor{black}{#2}\right]}}
\newcommand{\myctxr}[2]{{#1\left[\textcolor{black}{#2}\right]}}
\newcommand{\freeze}[1]{\left\langle #1 \right\rangle}
\newcommand{\upd}[2]{[#1\mapsto #2]}
\newcommand{\rup}[2]{#1\setminus #2}
\newcommand{\restrict}[1]{\downarrow_{#1}}
\newcommand{\loc}{\ell}	
\newcommand{\myloc}[2]{#1\left\{#2\right\}}	
\newcommand{\lbl}{l}	
%\newcommand{\nil}{\epsilon}

%% example
\newcommand{\epS}{\ep{s}{\mathtt{S}}}
\newcommand{\pS}{\ensuremath{\mathtt{S}}\xspace}
\newcommand{\epA}{\ep{s}{\mathtt{A}}}
\newcommand{\pA}{\ensuremath{\mathtt{A}}\xspace}
\newcommand{\epB}{\ep{s}{\mathtt{B}}}
\newcommand{\pB}{\ensuremath{\mathtt{B}}\xspace}
\newcommand{\epC}{\ep{s}{\mathtt{C}}}
\newcommand{\pC}{\ensuremath{\mathtt{C}}\xspace}
\newcommand{\exBook}{\text{`Logicomix'}}

%% global types
\newcommand{\gend}{\mathtt{end}}
\newcommand{\lend}{\mathsf{end}}
\newcommand{\gpart}[1]{\mathtt{#1}}
\newcommand{\gtact}[5]{\gpart{#1}\to\gpart{#2}:\{#3\langle #4\rangle.#5\}_{i \in I}}
\newcommand{\gtactp}[5]{\gpart{#1}\to\!\past \gpart{#2}:#3\langle #4\rangle.#5}
\newcommand{\gtactpp}[3]{\gpart{#1}\to \gpart{#2}: \past#3}
\newcommand{\gtcho}[4]{\gpart{#1}\to\gpart{#2}:\{#3:#4\}_{i \in I}}
\newcommand{\gtchoi}[5]{\gpart{#1}\to\gpart{#2}:\{#3{:}#4\}_{#5}}
\newcommand{\gtcom}[4]{\gpart{#1}\to\gpart{#2}:\langle #3\rangle.#4}

\newcommand{\lsend}[4]{\gpart{#1}!\{#2\langle #3\rangle.#4\}_{i \in I}}
\newcommand{\lrecv}[4]{\gpart{#1}?\{#2\langle #3\rangle.#4\}_{i \in I}}

%%%% NEW LOCAL TYOES
\newcommand{\ltout}[3]{\gpart{#1}!\langle#2\rangle.#3}
\newcommand{\ltinp}[3]{\gpart{#1}?\langle#2\rangle.#3}
\newcommand{\ltsel}[5]{\gpart{#1}\!\oplus\!\{#2: #3\}_{#4 \in #5}}
\newcommand{\ltbra}[5]{\gpart{#1}\&\{#2: #3\}_{#4 \in #5}}

%%%% NEW LOCAL TYOES, with cursor
\newcommand{\ltoutp}[3]{\gpart{#1}!\langle#2\rangle.\past #3}
\newcommand{\ltinpp}[3]{\gpart{#1}?\langle#2\rangle.\past #3}
\newcommand{\ltselp}[4]{\gpart{#1}\!\oplus\!\{#2\}_{#3 \in #4}}
\newcommand{\ltbrap}[4]{\gpart{#1}\&\{#2\}_{#3 \in #4}}



\newcommand{\tproj}[2]{#1\!\downarrow_{#2}}
\newcommand{\pproj}[3]{[\![#1]\!]^{#3}\downarrow_{#2}}

%stack based context%
%\newcommand{\conf}[2]{\Lbag #1 \; ; #2\; \Rbag}
\newcommand{\conf}[2]{\lbag #1 \; \textcolor{magenta}{\textbf{;}}\; #2 \rbag}
\newcommand{\stack}[1]{\mathtt{#1}}

%reductions%

\newcommand{\fwg}{\ensuremath{\fwcolor{\,\hookrightarrow\,}}}
\newcommand{\fwgs}{\ensuremath{\fwcolor{\,\hookrightarrow^*\,}}}
\newcommand{\bkg}{\ensuremath{\bkcolor{\,\rightharpoonup\,}}}
\newcommand{\bkgs}{\ensuremath{\bkcolor{\,\rightharpoonup^*\,}}}

\newcommand{\fw}{\ensuremath{\fwcolor{\,\twoheadrightarrow\,}}}
\newcommand{\fws}{\ensuremath{\fwcolor{\,\twoheadrightarrow^*\,}}}
\newcommand{\bk}{\ensuremath{\bkcolor{\,\rightsquigarrow\,}}}
\newcommand{\bks}{\ensuremath{\bkcolor{\,\rightsquigarrow^*\,}}}

\newcommand{\bkk}{\ensuremath{\bkcolor{\,\rightsquigarrow^{\,j}\,}}}
\newcommand{\trans}[1]{#1^{*}}
\newcommand{\refl}[1]{#1^{+}}
\newcommand{\fwa}{\ensuremath{\fwcolor{\Rrightarrow}}}
\newcommand{\lfwa}[1]{\xRightarrow{#1}}
\newcommand{\reda}{\rightarrowtail}
\newcommand{\lreda}[1]{\xRightarrow{#1}}

%equivalences%
%\newcommand{\bf}{\stackrel{\cdot}{\sim}}
%\newcommand{\bfw}{\stackrel{\cdot}{\approx}}
\newcommand{\bfb}{\sim}
\newcommand{\bfbw}{\approx}
\newcommand{\congruence}[1]{\stackrel{\cdot}{#1}}
\newcommand{\bka}{\ensuremath{\bkcolor{\Lleftarrow}}}
\newcommand{\lbka}{\xrightleftharpoons}

\newcommand{\ltrans}[1]{\xleftrightarrow{#1}}
%\newcommand{\simred}{\leftrightarrow}
\newcommand{\memstamp}{\eta}

\newcommand{\initC}[3]{\ensuremath{\mathcal{I}_{\,#3}^{#2}(#1)}}
\newcommand{\trad}[1]{\llbracket#1\rrbracket}

%stable conf%
\newcommand{\stable}{\mathtt{sb}}
\newcommand{\stables}[1]{#1\text{-}\stable}

\newcommand{\trace}{\rho}
\newcommand{\etrace}{\varepsilon}
\newcommand{\causeq}{\asymp}
\newcommand{\nottrace}[1]{{#1}_\bullet}
\newcommand{\tsource}[1]{\mathtt{src}(#1)}
\newcommand{\ttarget}[1]{\mathtt{trg}(#1)}

%%
\newcommand{\st}{\,|\,}
%jorge global macro%
\newcommand{\adeq}[2]{#1 \bowtie #2}
\newcommand{\ladeq}[3]{#1 \bowtie_{\,#3} #2}
\newcommand{\gth}[1]{\mathsf{#1}}
\newcommand{\ifk}{\mathbf{if}}
\newcommand{\thenk}{\mathbf{then}}
\newcommand{\elsek}{\mathbf{else}}
\newcommand{\ifproc}[3]{\ifk\,#1\, \thenk\, #2\,\elsek\,#3 }
\newcommand{\party}[1]{\ensuremath{\mathtt{#1}}\xspace}
\newcommand{\bigvect}[1]{\widehat{#1}}
\newcommand{\names}[1]{\mathtt{\mathbf{roles}}(#1)}


revchor-body.tex
% !TEX root = revchor-TR.tex

\section{Introduction}
This paper is about \emph{reversible computation} in the context of  models of concurrency for \emph{communication-centric} software systems, i.e., 
collections of distributed software components whose 
concurrent interactions 
are governed by reciprocal dialogues or \emph{protocols}.

Building upon process calculi techniques, 
these 
models  provide a rigorous footing for %programming languages featuring 
message-passing concurrency; on top of them, many (static) analysis techniques based on \emph{(behavioral) types}  and \emph{contracts} have been put forward  
to enforce key safety and liveness properties~\cite{DBLP:journals/csur/HuttelLVCCDMPRT16}. Reversibility is an appealing notion in concurrency at large~\cite{DBLP:journals/eatcs/Lanese14}, but especially so in communication-centric scenarios: it may elegantly abstract fault-tolerant communicating systems that react to  unforeseen circumstances (say, local failures) by ``undoing'' computation steps so as to reach a consistent previous state.
%As such, reversibility is related to process constructs such as exceptions, compensations,  and transactions (see, e.g.,~\cite{DBLP:conf/concur/DanosK05,DBLP:conf/concur/CarboneHY08,DBLP:conf/concur/VriesKH10,DBLP:books/sp/sensoria2011/FerreiraLRVZ11}).
%\jp{I would try to mention/cite connections between `declarative programming' and reversibility here.}

In communication-centric software systems, protocols
specify the intended communication structures among interacting components. 
We focus on process calculi equipped with behavioral types, which use those protocols as types to enforce communication correctness. The interest is in different flavors of \emph{protocol conformance}, i.e., properties that ensure that each component respects its ascribed protocol. The integration of reversibility in models of communication-centric systems has been addressed from various angles (cf. \cite{DBLP:journals/jlp/TiezziY15,DBLP:conf/rc/TiezziY16,DBLP:journals/fac/BarbaneraDd16,DBLP:journals/corr/MezzinaP16}). Focusing on \emph{session types}~\cite{honda.vasconcelos.kubo:language-primitives,HYC08} (a well established class of behavioral types), Tiezzi and Yoshida~\cite{DBLP:journals/jlp/TiezziY15} were the first to integrate reversibility into a session $\pi$-calculus, following the seminal approach of Danos and Krivine~\cite{DanosK04}; in~\cite{DBLP:journals/jlp/TiezziY15}, however, session types are not used in the definition of reversible communicating systems, nor play a role in establishing their properties. 

Triggered by this observation,  our prior work~\cite{DBLP:journals/corr/MezzinaP16,MezzinaP17} develops a \emph{monitors-as-memories} approach. The idea is to use \emph{monitors} (run-time entities that enact protocol actions) as the \emph{memories} needed to record  and   undo communication steps. 
There is a monitor for each protocol participant; 
the monitor includes a session type that describes the intended protocol. 
We use a  \emph{cursor}  to ``mark'' the current protocol state in the type; the cursor can move to the future (enacting protocol actions) but also to the past (reversing protocol actions). The result is a streamlined process framework in which the key properties of a reversible semantics can be established with simple proofs,
because session types narrow down the spectrum of possible process behaviors, allowing only those forward and backward actions that correspond to the declared protocols.
The most significant of such properties is 
\emph{causal consistency}~\cite{DanosK04},   considered as the ``right''  criterion for reversing concurrent processes~\cite{DBLP:journals/eatcs/Lanese14}. 
Intuitively, causal consistency ensures that reversible steps lead to system states that could been have reached by performing forward steps only. That is, causally consistent reversibility does not lead to extraneous states, not reachable through ordinary computations.

The  framework in~\cite{DBLP:journals/corr/MezzinaP16,MezzinaP17}, however,  accounts only for reversible  $\pi$-calculus processes implementing \emph{binary sessions}, i.e., protocols between exactly two partners. Also, it considers \emph{synchronous communication} instead of the more general (and practical) \emph{asynchronous (queue-based) communication}. 
Hence, our prior work %does not cover the 
%\emph{multiparty asynchronous sessions}~\cite{HYC08} that may describe protocols between two or more parties. Thus,~\cite{DBLP:journals/corr/MezzinaP16} 
rules out an important class of real-life protocols, namely the 
\emph{choreographies} that  describe  interaction scenarios among multiple parties without a single point of control. 
In \emph{multiparty session types}~\cite{HYC08}, these choreographies are represented by a \emph{global type} that can be projected as \emph{local types} to obtain each participant's contribution to the entire interaction. 
Moving from binary to multiparty sessions is a significant jump in expressiveness;
\added{in fact, global types offer a convenient declarative description of the entire communication scenario.}
However, the multiparty case also  
entails added challenges, as  two levels of abstraction, global and local, should be considered for (reversible) protocols and their   implementations. Hence, it is far from obvious that our monitors-as-memories approach to reversibility and  causal consistency extend to the multiparty case.
%\footnote{Indeed, the principled transfer of  techniques from binary to multiparty settings has been clarified only recently~\cite{DBLP:conf/forte/CairesP16}.}

%\paragraph{Contributions} 
%The \emph{main contribution} of this paper is the extension of the monitors-as-memories approach to multiparty asynchronous sessions. 
This paper makes the following contributions:
\begin{enumerate}[1.]
\item We introduce a process model for reversible, multiparty sessions with asynchrony (as in~\cite{DBLP:journals/mscs/KouzapasYHH16}), process passing~\cite{SangiorgiD:expmpa,KPY2016} and decoupled rollbacks (\S\,\ref{sec:calculus}). 
We define forward and backward semantics for multiparty processes by extending the monitors-as-memories approach to both
global types and their implementations. 

\item  We prove that reversibility in our model is causally consistent (Theorem~\ref{t:causal}). The proof is challenging as we must appeal to an alternative reversible semantics with 
\emph{atomic rollbacks}, which we show to coincide with the decoupled rollbacks (Theorem~\ref{t:bf}). 

\item We formally connect reversibility at the (declarative) level of global types
and that at the (operational) level of processes monitored by local types with cursors (Theorem~\ref{t:corrgc}).
\end{enumerate}

%, so we improve over our prior work already at the level of processes. 
\noindent 
We stress that asynchrony, process passing, and decoupled rollbacks are not considered in prior works~\cite{DBLP:conf/rc/TiezziY16,DBLP:journals/corr/Dezani-Ciancaglini16a,DBLP:journals/corr/MezzinaP16,MezzinaP17}.
Asynchrony  and decoupled rollbacks are delicate issues in a reversible multiparty setting---we do not know of other asynchronous calculi with reversible semantics, nor featuring the same combination of constructs. 
The formal connection between global and local levels of abstraction (Theorem~\ref{t:corrgc}) is also unique to our multiparty setting.



%\paragraph{Related Work}
%Prior works on reversible multiparty sessions 
%feature less expressive languages, 
%follow different approaches, or obtain results of different relevance. 
%Tiezzi and Yoshida~\cite{DBLP:conf/rc/TiezziY16} study
%the cost of implementing 
%different ways of reversing binary and multiparty sessions; 
%since they work in a \emph{synchronous} setting, 
%these alternatives are simpler or incomparable to our asynchronous, decoupled rollback.
%Dezani-Ciancaglini and Giannini~\cite{DBLP:journals/corr/Dezani-Ciancaglini16a} develop typed multiparty sessions with \emph{checkpoints},  points in the global protocol to which computation may return.   
%While our reversible actions  are embedded in/guaranteed by the operational semantics, rollbacks in~\cite{DBLP:journals/corr/Dezani-Ciancaglini16a} should specify the name of the checkpoint to which computation should revert.
%In their approach, defining reversibility requires modifying both processes and types. In contrast, we consider standard processes and  local types (with cursors) as monitors. 
%While we show causal consistency with a direct proof, in~\cite{DBLP:journals/corr/Dezani-Ciancaglini16a} causal consistency follows indirectly, as a consequence of typing. 
%Reversibility in our model is fine-grained in that we allow reversible actions concerning exactly two of the protocol participants; in~\cite{DBLP:journals/corr/Dezani-Ciancaglini16a} when a checkpoint is taken, also parties not related with that choice are forced to return to a checkpoint. Barbanera et al. have studied reversible/retractable contracts from different perspectives~\cite{DBLP:journals/corr/BarbaneraDd14,BDLL15,DBLP:conf/coordination/Barbanerad16}. 
%Although behavioral types and contracts are conceptually similar, there are technical differences that make in-depth comparisons hard to obtain.

\paragraph{Organization}
This paper is organized as follows. In \S\,\ref{sec:calculus}, we introduce our process model of reversible choreographies. 
We illustrate the model by means of an example in \S\,\ref{s:examp}.
In \S\,\ref{s:res} we establish causal consistency by relating decoupled and atomic semantics, and connect reversibility at global and local levels. 
%\S\,\ref{s:ext} discusses extensions to our framework, while 
\S\,\ref{s:rw} contrasts with related works, while
\S\,\ref{s:conc} collects some concluding remarks. 
%\emph{For the sake of space, some definitions/proofs are relegated to the appendix.}
\emph{The appendix contains additional material.}

\section{Reversible Choreographies}
\label{sec:calculus}

%\begin{figure}
%\begin{center}
%    \includegraphics[width=8.7cm]{./img/figmodel.pdf}
%\end{center}
%\vspace{-4mm}
%\caption{Our process model of multiparty communications.}\label{f:model}
%\end{figure}
%Fig.~\ref{f:model} depicts the ingredients of our
%two-level model of \emph{choreographies} and \emph{configurations/processes}.
Choreographies are defined in terms of \emph{global types}, which declaratively describe a protocol among two or more participants. 
A global type can be \emph{projected} onto each participant so as to obtain 
its corresponding  \emph{local type}, i.e., a session type that abstracts a participant's contribution to the global protocol. 
(Below we often use `choreographies' and `global types' as synonyms.)
The semantics of global types is given in terms of forward and backward  transition systems (Fig.~\ref{f:gts}). 
There is a \emph{configuration} for each protocol participant: it includes a \emph{located process}
that 
 specifies asynchronous communication behavior, subject to a \emph{monitor}
that enables forward/backward steps at run-time
based on the local type.
The semantics of configurations is given in terms of forward and backward reduction relations (Figs.~\ref{fig:fw} and~\ref{fig:bk}).
% standardly coupled with a structural congruence on configurations/processes.

\begin{remark}[Colors]
Throughout the paper, we  use colors to improve readability. 
In particular, %we use colors to distinguish the elements for forward and backward semantics:
elements in \fwcolor{blue} belong to a forward semantics;
elements in \bkcolor{red} belong to a backward semantics.
\end{remark}
%Given this two-level setting, our goal will be that of connecting (i)~forward and backward steps at the (high) level of choreographic specifications, and (ii) forward and backward steps at the (low) level of configurations/processes. This will be content of 
%Theorem~\ref{t:corrgc}.

\subsection{Global and Local Types}

\subsubsection{Syntax}
Let us write $\p, \q, \gpart{r}, \pA, \pB \ldots$ to denote (protocol) \emph{participants}.
The syntax of global types ($G, G', \ldots$) and local types  ($T, T', \ldots$) is standard~\cite{HYC08} and defined as follows:
\begin{align*}
			G, G'  \bnfis & \gtcom{p}{q}{U}{G} \bnfbar \gtcho{p}{q}{\lbl_i}{G_i} \\
			\bnfbar & \mu X. G \bnfbar X \bnfbar \gend \\
			U, U'  \bnfis & \bool \bnfbar \nat \bnfbar \cdots %\bnfbar T 
			\bnfbar \shot{T} \\
	    	T, T'  \bnfis & \ltout{p}{U}{T} \sbnfbar \ltinp{p}{U}{T} \\
		  \sbnfbar & \ltsel{p}{\lbl_i}{T_i}{i}{I} \sbnfbar \ltbra{p}{\lbl_i}{T_i}{i}{I}   
		 %\lsend{p}{\lbl_i}{U_i}{T_i} \bnfbar \lrecv{q}{\lbl_i}{U_i}{T_i} \bnfbar 
		\sbnfbar \mu X. T \sbnfbar X \sbnfbar \lend 
\end{align*}
\noindent
Global type $\gtcom{p}{q}{U}{G}$ says that \p may send a value of type $U$ to \q, and then continue as $G$.
Given a finite \added{index set} $I$ and pairwise different \emph{labels} $\lbl_i$, 
global type $\gtcho{p}{q}{\lbl_i}{G_i}$
 specifies that 
 \p may choose 
label $\lbl_i$, communicate this selection to \q, and then continue as $G_i$. 
In these two types %thus denote direct communications; 
we assume that $\p \neq \q$.
Global %types include also 
recursive and terminated protocols are denoted $\mu X. G$ and $\gend$, respectively.
We write $\parties{G}$ to denote the set of participants in $G$.
Value types $U$ include basic first-order values (constants),   but also \emph{higher-order} values: abstractions from names to processes. 
(We write $\Proc$ to denote the type of processes.)
Local types 
%abstract the behavior of individual participants. Types 
$\ltout{p}{U}{T}$ and $\ltinp{p}{U}{T}$ denote, respectively, an output and input of value of type $U$ by \p.
\added{We use  $\alpha$ to denote type prefixes  $\typeIn{\p}{U}$, $\typeOut{\p}{U}$.}
Type $\ltbra{p}{\lbl_i}{T_i}{i}{I}$ says that \p 
offers different behaviors, available as labeled alternatives;
conversely, type $\ltsel{\p}{\lbl_i}{T_i}{i}{I}$ 
says that \p may select one of such alternatives. Terminated and recursive local types are denoted $\lend$ and $\mu X. T$, respectively. 

\added{As usual, we consider only recursive types $\mu X. G$ (and $\mu X. T$) in which $X$ occurs guarded in $G$ (and $T$).}
 We shall take an equi-recursive view of (global and local) types, and so we consider two  types with the same regular tree as equal.
 
Global and local types are connected by  \emph{projection}:
following~\cite{HYC08},
the projection of $G$ onto participant $\p$, written $\tproj{G}{\p}$, is defined in Fig.~\ref{f:proj}. 
\added{Projection for $\gtcho{p}{q}{l_i}{G_i}$ is noteworthy: 
the projections of the participants not involved in the choice (different from $\p, \q$) should correspond to the same identical local type.}
\begin{figure}[t!]
{%\small
\begin{align*}
\tproj{(\gtcom{p}{q}{U}{G})}{\gpart{r}} & = 
\begin{cases}
\ltout{\q}{U}{(\tproj{G}{\gpart{r}})} & \text{if $\gpart{r} = \gpart{p}$} \\
\ltinp{\p}{U}{(\tproj{G}{\gpart{r}})} & \text{if $\gpart{r} = \gpart{q}$} \\
(\tproj{G}{\gpart{r}}) &  \text{if $\gpart{r} \neq \gpart{q}, \gpart{r} \neq \gpart{p}$}
\end{cases}
\\
\tproj{(\gtcho{p}{q}{l_i}{G_i})}{\gpart{r}}  & = 
\begin{cases}
\ltsel{\q}{\lbl_i}{(\tproj{G_i}{\gpart{r}})}{i}{I}  & \text{ if $\gpart{r} = \gpart{p}$} \\
\ltbra{\p}{\lbl_i}{\tproj{G_i}{\gpart{r}}}{i}{I}  & \text{ if $\gpart{r} = \gpart{q}$} \\
(\tproj{{G_1}}{\gpart{r}}) &  \text{ if $\gpart{r} \neq \gpart{q}, \gpart{r} \neq \gpart{p}$ and} \\ 
& \text{~~$\forall i, j \in I. \tproj{{G_i}}{\gpart{r}} = \tproj{{G_j}}{\gpart{r}}$}
\end{cases}
\\
\tproj{(\mu X. G)}{\gpart{r}} &= 
\begin{cases}
\mu X. \tproj{G}{\gpart{r}} & \text{if $\gpart{r}$ occurs in $G$}
\\
\lend & \text{otherwise}
\end{cases}
\\
\tproj{X}{\gpart{r}} & = X
\qquad
\tproj{\gend}{\gpart{r}} = \lend
\end{align*}
}
\vspace{-4mm}
\caption{Projection of a global type $G$ onto a participant $\gpart{r}$.\label{f:proj}}
\end{figure}

\subsubsection{Semantics of Choreographies}\label{ss:chore}
\input{semglobal}
The semantics of global types (Fig.~\ref{fig:prot_sem})
comprises forward and backward transition rules. 
%\jp{Indeed, our semantics seems more like an ``unlabeled LTS''. Could it be that labels will be useful later on?}
To express backward steps, we require some auxiliary notions.
We use \emph{global contexts}, ranged over by $\ctx{G}, \ctx{G}', \ldots$ with holes $\bullet$,  to record
previous actions, including the choices discarded and committed:
%\begin{center}
$$
\ctx{G}
\bnfis   
\bullet 
\sbnfbar  
\ctx{G}[\gtcom{p}{q}{U}{\ctx G}]
\sbnfbar
\ctx{G}[\gpart{p}\to\gpart{q}:\{\lbl_i:G_i \,;\, \lbl_j:\ctx{G}\}_{i \in I\setminus j} ]
$$
%\end{center}
We also use \emph{global types with history}, ranged over by $\mathsf{H}, \mathsf{H}', \ldots$, 
  to record the current protocol state. 
This state is denoted by the \emph{cursor}~$\past$, which we introduced in~\cite{DBLP:journals/corr/MezzinaP16}:
\begin{align*}
%			G, G'  \bnfis & \gtact{p}{q}{\lbl_i}{U_i}{G_i} \bnfbar \mu X. G \bnfbar X \bnfbar \gend \\
%			\bnfbar & \past G \bnfbar \gpart{p}\to\!\past\gpart{q}:\{l_i\langle U_i\rangle.G_i \,;\, l_j\langle U_j\rangle.G_j\}_{i \in I\setminus j} \\
%			\bnfbar & \gpart{p}\to\gpart{q}:\{l_i\langle U_i\rangle.G_i \,;\, l_j\langle U_j\rangle.\past G_j\}_{i \in I\setminus j}
			\mathsf{H}, \mathsf{H}'  \bnfis & %\gtact{p}{q}{\lbl_i}{U_i}{G_i} \bnfbar \mu X. G \bnfbar X \bnfbar \gend \\
			%\bnfbar & 
			\past G \bnfbar	G \past 
			\bnfbar 
			\gtcom{p}{\!\!\past q}{U}{G} 
			\bnfbar 
			\gtcom{p}{q}{U}{\past G} \\
			\bnfbar & 
			\gpart{p}\to\!\!\past\gpart{q}:\{\lbl_i:G_i \,;\, \lbl_j:G_j\}_{i \in I\setminus j} 
			\\
			\bnfbar & 
 			\gpart{p}\to\gpart{q}:\{\lbl_i:G_i \,;\, \lbl_j:\past G_j\}_{i \in I\setminus j}  
\end{align*}
%Projection and notation $\parties{\cdot}$ extend easily to global types $\gth{H}$ (cf. Fig.~\ref{f:projext}).
%Notation $\parties{\cdot}$ extends easily to global types $\gth{H}$.
Intuitively,  directed exchanges such as $\gtcom{p}{q}{U}{G}$ have three \emph{intermediate states},
characterized by the decoupled involvement of \p and \q in the intended asynchronous model.
The \emph{first state}, denoted $\past \gtcom{p}{q}{U}{G}$, describes the situation prior to the exchange.
The \emph{second state} represents the point in which \p has sent a value of type $U$ but this message has not yet
reached \q; this is denoted $\gtcom{p}{\!\!\past q}{U}{G}$.
The \emph{third state} represents the point in which \q has received the message from \p and
the continuation $G$ is ready to execute; this is denoted by $\gtcom{p}{q}{U}{\past G}$.
These intuitions extend to $\gtcho{p}{q}{l_i}{G_i}$, with the following caveat:
the second state should distinguish the choice made by $\p$ from the discarded alternatives; 
  we write $\gpart{p}\to\!\!\past\gpart{q}:\{\lbl_i:G_i \,;\, \lbl_j:G_j\}_{i \in I\setminus j}$ to describe that $\p$ has selected $\lbl_j$ and that this choice is still to be received by \q. Once this occurs, a state
  $\gpart{p}\to\gpart{q}:\{\lbl_i:G_i \,;\, \lbl_j:\past G_j\}_{i \in I\setminus j}$ is reached.

These  intuitions come in handy to describe the forward and backward transition rules
in Fig.~\ref{fig:prot_sem}. 
For a forward directed exchange of a value, 
Rule~\fwcolor{\textsc{(FVal1)}} formalizes the transition from the first   to the second state;
Rule~\fwcolor{\textsc{(FVal2)}} denotes the transition from the second to the third state.
Rules~\fwcolor{\textsc{(FCho1)}} and~\fwcolor{\textsc{(FCho2)}} are their analogues for the forward directed communication of a label.
Rules~\bkcolor{\textsc{(BVal1)}} and~\bkcolor{\textsc{(BVal2)}} undo the step performed by 
Rules~\fwcolor{\textsc{(FVal1)}} and~\fwcolor{\textsc{(FVal2)}}, respectively. 
Also, 
Rules~\bkcolor{\textsc{(BCho1)}} and~\bkcolor{\textsc{(BCho2)}} undo the step performed by 
Rules~\fwcolor{\textsc{(FCho1)}} and~\fwcolor{\textsc{(FCho2)}}, respectively. 




\subsection{Processes and Configurations}
\label{subsec:syntax}
\input{syntax}

\subsubsection{Syntax}
The syntax of processes and configurations is given in \figref{fig:syntax}.
For processes $P, Q, \ldots$ we
follow closely the syntax of \HOp, the core higher-order session $\pi$-calculus~\cite{KPY2016}.
%(In turn, \HOp is a subcalculus of the higher-order language studied  in~\cite{tlca07}.) 
The syntax of configurations builds upon that of processes.
%Next, we describe all these syntactic elements.

%\myparagraph{Values}
\emph{Names} $a,b,c$ (resp.~$s, s'$) 
range over shared (resp. session) names. 
We use session names indexed by  {participants}, denoted $\ep{s}{\p}, \ep{s}{\q}$. 
Names $n, m$ are session or shared names.
\added{First-order values  $v, v'$ include base values and constants.}
%Dual endpoints are $\dual{n}$ with $\dual{\dual{s}} = s$ and $\dual{a} = a$.
%We define the dual operation over names $n$ as $\dual{n}$ with
%$\dual{\dual{s}} = s$ and $\dual{a} = a$.
%Intuitively, names $s$ and $\dual{s}$ are dual (two) \emph{endpoints} while 
%shared names represent shared (non-deterministic) points. 
Variables are denoted by $x, y$, 
and recursive variables are denoted by $\varp{X}, \varp{Y}$.
The syntax of values $V$ includes shared names, first-order values, but also 
name abstractions (higher-order values)
$\abs{x}{P}$,   where $P$ is a process.
\added{As shown in~\cite{KPY2016}, abstraction passing suffices to express name passing (\emph{delegation}).}
%Symbols $u, v, \dots$ range over identifiers; and  $V, W, \dots$ to denote values. 
%\emph{Values} $V,W$ include 
%identifiers  %(first-order values) 
%and 
%abstractions $\abs{x}{P}$ (first- and higher-order values, resp.). 

%\myparagraph{Terms} 

%\jp{This needs to be adjusted, we have a more general selection construct; also, we need to decide about parallel...}

Process terms include   prefixes for sending and receiving values $V$, written 
$\bout{u}{V} P$ and $\binp{u}{x} P$, respectively.
\added{Given a finite index set $I$,}
processes $\bsel{u}{\lbl_i. P_i}_{i\in I}$ and $\bbra{u}{l_i: P_i}_{i \in I}$ implement 
selection and branching (internal and external labeled choices, respectively). 
The selection  $\bsel{u}{\lbl_i. P_i}_{i\in I}$ is actually 
a non-deterministic choice over $I$.
In an improvement with respect to~\cite{DBLP:journals/corr/MezzinaP16,MezzinaP17}, here we consider parallel composition of processes $P \Par Q$ 
and recursion $\recp{X}{P}$ (which binds the recursive variable $\varp{X}$ in process $P$).
%as we will discuss, adding these constructs entails challenges in the characterization of 
%causal consistent semantics (see next section).
Process 
$\appl{V}{u}$ 
is the application
which substitutes name $u$ on the abstraction~$V$. %; our semantics will ensure that $V$ is not a name.
Constructs for 
name restriction $\news{n} P$ and 
inaction $\inact$ are standard.
Session restriction $\news{s} P$ simultaneously binds all the participant endpoints in $P$.
We write $\fv{P}$ and $\fn{P}$%, and $\sn{P}$ 
to denote the sets of free 
variables 
and names in $P$.
We assume $V$ in $\bout{u}{V}{P}$ does not include free recursive 
variables $\rvar{X}$.
If $\fv{P} = \emptyset$, we call $P$ {\em closed}.


%\\
The syntax of configurations $M, N, \ldots$, includes  inaction $\inact$, the parallel composition  $M \Par N$,
and name restriction $\news{n} M$. 
Also, it includes constructs for \emph{session initiation}: 
configuration $\myloc{\loc}{\bout{a}{x}{P}}$ denotes the \emph{request} of a service identified with $a$ implemented in 
$P$ as $x$; conversely, configuration 
$\myloc{\loc}{\binp{a}{x}{P}}$
denotes service \emph{acceptance}. In both constructs,  identifiers $\loc, \loc', \ldots$ denote    a  process \emph{location} 
or  \emph{site} (as in, e.g., the distributed $\pi$-calculus~\cite{Hennessy07}).
%\jp{This is just to set up some terminology, the text needs to be polished:} 

Configurations also include the following \emph{run-time elements}: %, not part of ``source'' processes:
\begin{enumerate}[$\bullet$]
\item \emph{Running processes} are of the form $\np{\loc}{\conf{\stack C}{P}}$, where $\loc$ is a location that 
hosts a process $P$ and a \emph{(process) stack} $\stack{C}$.
A process stack is simply a list of processes, useful 
%, as defined by the  grammar:
%$
%\stack{C} \bnfis  \inact \sbnfbar \bsel{u}{\lbl_i. P_i}_{i\in I} \sbnfbar 
%\bbra{u}{ \lbl_i:P_i}_{i \in I} \sbnfbar \stack{C}_1, \stack{C}_2
%$.
%Process stacks
  to record/reinstate the discarded alternatives   in a labeled choice.

\item \emph{Monitors} are of the form $\monig{s}{H}{\mytilde{x}}{\store}$ 
where 
$s$ is the session being monitored, 
$H$ is a history session type (i.e. a session type with ``memory''), 
$\mytilde{x}$ is a set of free variables, 
and the \emph{store} $\store$  records the value of such variables (see Def.~\ref{d:store}).
These four elements allow us to track the current protocol
and  state of the   monitored process.
Each monitor has a 
\emph{tag} $\mytagg$, which can be either \emph{empty} (denoted `$\normark$') or \emph{full} (denoted `$\rmark$'). 
When first created all monitors have an empty tag; a full tag indicates that the running process associated to the monitor
is currently involved in a  decoupled reversible step.
\added{We often omit the empty tag 
(so we write 
$\moni{s}{H}{\mytilde{x}}{\store}$ instead of 
$\hmoni{s}{H}{\mytilde{x}}{\store}$)
and write $\monir{s}{H}{\mytilde{x}}{\store}$ to emphasize the reversible (red) nature of a 
monitor with full tag.}


\item Following~\cite{DBLP:journals/mscs/KouzapasYHH16}, we have \emph{message queues}
of the form 
%$\codah{s}{h_i}{h_o}{\restrict{\mytilde{\p}}}$,
$\codah{s}{h_i}{h_o}$,
where $s$ is a session, $h_i$ is the input part of the queue, and $h_o$ is the output part of the queue.
Each queue contains messages of the form $\valueq{\p}{\q}{\anyv}$ (read: ``message $\anyv$ is sent from $\p$ to $\q$'').
As we will see, the effect of an output prefix in a process is to place the message in its corresponding output queue;
conversely, the effect of an input prefix is to obtain the first message from its input queue. 
\added{Messages in the queue are \textit{never consumed}: a process reads a message $\valueq{\p}{\q}{\anyv}$ by moving it from the (tail of) queue $h_o$ to the (top of) queue $h_i$. This way, the    delimiter `$\history$' distinguishes the \textit{past} of the queue from its \textit{future}.}

%Also, $\mytilde{\p}$ denotes a sequence of participant identities currently involved in a reversible step; when this sequence is empty, we  write  $\codah{s}{h_i}{h_o}{~}$ instead of $\codah{s}{h_i}{h_o}{\restrict{\epsilon}}$.

\item We use \emph{running functions} of the form $\mem{k}{(\appl{V}{u})}{\loc}$ to reverse
 applications $\appl{V}{u}$. While $k$ is a fresh identifier (key) for this term, $\loc$ is the location of 
the running process that contains the application.

\end{enumerate}

\noindent
We shall write $\procs$ and $\confs$ to indicate the set of processes and configurations, respectively. 
We call \emph{agent} an element of the set $\agents = \confs \cup \procs$. 
We let $P, Q$  to range over $\procs$; also, we use $L,M,N$ to range over $\confs$ and $A,B,C$ to range over $\agents$.
%; and closed $P$ without 
%free session names a {\em program}. 




%The projection of global types into processes:
%\begin{align*}
%\pproj{\gtact{p}{q}{\lbl_i}{U_i}{G_i}}{\gpart{r}}{s} & = 
%\begin{cases}
%\lsend{p}{\lbl_i}{U_i}{\pproj{G_i}{\gpart{r}}{s}} & \text{if $\gpart{r} = \gpart{p}$} \\
%\lrecv{p}{\lbl_i}{U_i}{\pproj{G_i}{\gpart{r}}{s}} & \text{if $\gpart{r} = \gpart{q}$} \\
%\pproj{{G_1}}{\gpart{r}}{s} &  \text{if $\gpart{r} \neq \gpart{q}, \gpart{r} \neq \gpart{p}$}
%\end{cases}
%\\
%\pproj{\mu X. G}{\gpart{r}}{s} &= \mu X. \pproj{G}{\gpart{r}}{s}
%\qquad
%\pproj{X}{\gpart{r}}{s} = X
%\qquad
%\pproj{\gend}{\gpart{r}}{s} = \inact
%\end{align*}
%\jp{What is the role of $s$ in this projection?}




%Following~\cite{DBLP:journals/soca/CoppoDV15,Castellani2016},
%we define the 
% semantics of configurations by relying on a \emph{process collection} $\procs$, 
% which collects pairs $(P, T)$ of a process $P$ with its corresponding (local) type $T$. 
% The collection $\procs$ is used during session initiation, and so the semantics is parametric on $\procs$.
% We shall assume that process collections are \emph{complete}:
% for a given set $\mathcal{G}$ of global types if, for every $G \in \mathcal{G}$, there are processes in $\procs$ 
% whose types correspond to the local types obtained by projecting $G$ onto its participants.
%
%\begin{definition}\label{d:initc}
%Given a global type $G$ with 
%$\pa(G) = \{\p_1, \p_2, \ldots, \p_n\}$, a shared name $a$, 
%and a process collection $\procs$, we write 
%$\initC{G}{\procs}{a}$
%to denote the configuration defined as:
%$$\initC{G}{\procs}{a} = 
%\bout{a}{x:T_1}{P_{1}} \Par 
%\prod_{j \in \{2, \ldots, n\}}\binp{a}{x:T_j}{P_{j}} $$ 
%with 
%$T_i = \tproj{G\!}{\p_i}$ and 
%$(P_{i}, T_i) \in \procs$, for all 
%$i \in \{1, \ldots, n\}$. \\
%\jp{We may want to make this more general, so as to capure non-determinism.}
%\end{definition}


%\subsection{Operational Semantics}
%\label{subsec:semantics}


%\subsection{Local Operational Semantics}
%\label{subsec:sem}

\subsubsection{A Decoupled Semantics for Configurations}\label{ss:semconf}
We define a reduction relation on configurations, coupled with a structural congruence
 on processes and configurations.
Our reduction semantics defines a \emph{decoupled} treatment for reversing communication actions within a protocol.
Reduction is thus defined as $\red \subset \confs \times \confs$, whereas structural congruence is defined as $\scong\, \subset \procs^{2} \cup \confs^{2}$.  We require auxiliary definitions for \emph{contexts}, \emph{stores}, and \emph{type contexts}.

%\begin{definition}
\emph{Evaluation contexts} are configurations with one hole 
 `$\bullet$', as defined by the following grammar:
$$\ctx{E}\bnfis \bullet \bnfbar M\Par \ctx{E} \bnfbar \news{n}\, \ctx{E}$$
\emph{General contexts} $\ctx{C}$ are processes or configurations with one hole~$\bullet$: they are obtained  by replacing one occurrence of $\inact$ (either as a process or as a configuration) with $\bullet$.
%\end{definition}
%\noindent 
A congruence on processes and configurations is an equivalence  $\Re$ that is closed under general contexts: $P \,\Re\,  Q \Longrightarrow \myctx{C}{P}\,\Re\,  \myctx{C}{Q}$
and $M\Re N \Longrightarrow \myctx{C}{M}\,\Re\,  \myctx{C}{N}$.
We define $\equiv$  as the smallest congruence on processes and configurations
that satisfies rules in Fig.~\ref{fig:str}.
A relation $\Re$ on configurations is \emph{evaluation-closed} if it satisfies the   following rules:
\begin{mathpar}
 \inferrule*[left=(Ctx)]{M\,\Re\, N}{\myctx{E}{M}\,\Re\, \myctx{E}{N}} \and 
 \inferrule*[left=(Eqv)]{M \scong M' \and M' \,\Re\, N' \and N'\scong N}{M \,\Re\, N} \and 
\end{mathpar}

\begin{figure}[t!]
{%\small
\[
	\begin{array}{c}
		A \Par \inact \scong A
		\quad
		A \Par B \scong B \Par A
		\quad
		A \Par (B \Par C) \scong (A \Par B) \Par C
%		\\[1mm]
%		\quad 
		\\[1mm]
		A \Par \news{n} B \scong \news{n}(A \Par B)
		\ (n \notin \fn{P})
				\quad
		\news{n} \inact \scong \inact
		\\[1mm]
		\recp{X}{P} \scong P\subst{\recp{X}{P}}{\rvar{X}}
%		\\[1mm]
		\quad
		A \scong B \textrm{ if } A \scong_\alpha B
%		\qquad
%		\dk{V \scong W \textrm{ if } V \scong_\alpha W
%\quad \abs{x}{P} \scong \abs{x}{Q} \textrm{ if } P \scong Q} 
%\quad
%	\np{\key{k}{i}}{(P \Par Q)} \scong \np{\key{k}{i}}{P} \Par \np{\key{k}{i}}{Q}
	\end{array}
\]
}
\vspace{-4mm}
\caption{Structural Congruence}
\label{fig:str}
\end{figure}
%To enable reversible labeled choices, we define the following class of \textit{choice contexts}:
%
%\begin{definition}[Choice context]
%\textit{Choice contexts} are processes with one hole, denoted ``$\bullet$'', and defined by the following grammar:
%%\begin{align*}
%%& \ctx{K},\ctx{H} \bnfis \quad \bullet \sbnfbar 
%%\bsel{u}{\lbl_w}\ctx{K} + \freeze{\sum_{i\in I\setminus w}\bsel{u}{\lbl_i} P_i} \sbnfbar 
%%\bbra{u}{\lbl_w:\ctx{K} \,,\, \freeze{\lbl_i:P_i}}_{i \in I\setminus w}
%%\end{align*}
%\begin{align*}
%& \ctx{K},\ctx{H} \bnfis \quad \bullet \sbnfbar 
%\ctx{K} + \freeze{\sum_{i\in I}\bsel{u}{\lbl_i} P_i} \sbnfbar 
%\bbra{u}{\ctx{K} \,,\, \freeze{\lbl_i:P_i}}_{i \in I}
%\end{align*}
%\end{definition}

%\noindent
The state of monitored processes is formalized as follows:

\begin{definition} \label{d:store}
A store $\store$ is a mapping from variables to values. Given a store $\store$, a variable $x$, and a value $V$, 
the \emph{update} $\store\upd{x}{V}$ and the 
 \emph{reverse update} $\rup{\store}{x}$ are defined as follows:
%\cm{we have to understand better this thing of all bound variables are different }
\begin{align*}
\store\upd{x}{V} & = \begin{cases}
\store\cup \{(x,V)\} &\text{ if } x\not\in \mathtt{dom}(\store) \\ 
\text{ undefined }  & \text{otherwise}
\end{cases} 
\\
\rup{\store}{x} & =  \begin{cases}
\store_1 &\text{ if } \store=\store_1\cup \{(x,V)\} \\ 
\store  & \text{otherwise}
\end{cases} 
\end{align*}
\end{definition}

\noindent Together with local types with history, the following notion of type context allows us to record the current protocol state:
\begin{definition} 
\added{Let $k, k', \ldots$ denote fresh name identifiers.} We define 
\textit{type contexts} as (local) types with one hole, denoted ``$\bullet$'':
\begin{align*}
 \ctx{T},\ctx{S}   \bnfis  &  \bullet  \sbnfbar
 \q\btsel{\lbl_w:\ctx{T} \;;\; \lbl_i:S_i}_{i \in I\setminus w} \sbnfbar \q\btbra{\lbl_w:\ctx{T} \, , \, \lbl_i:S_i}_{i \in I\setminus w}
 \\
  \sbnfbar &  \alpha.\ctx{T} \sbnfbar    k.\ctx{T} \sbnfbar (\loc,\loc_1,\loc_2).\ctx{T} 
\end{align*}
%\cm{They are no more types, because of $k$. Moreover we can compact $k$.T and $(k,k_1,k_2).T$ with $\tilde{k}$ but as to be an ordered list}
%\cm{Dire cosa sono $k$ and $\loc$}
\end{definition}
\added{\noindent Type contexts $k.\ctx{T}$ 
and $(\loc,\loc_1,\loc_2).\ctx{T}$ 
will be instrumental in formalizing reversibility of
name applications and thread spawning, respectively, which are not described by local types.}


%%% ==== START QUEUE EQUIVALENCE
%\begin{definition}[Equivalence on message queues]
%%\cm{Not sure we need this, otherwise we have that $a \rightarrow b; c \rightarrow d = c \rightarrow d; a \rightarrow b$}
%%\jp{I have modified this.}
%%Let $m$ stand for either $V$ or $\lbl$. 
%We define the structural equivalence on queues, denoted $\equivq$, as follows:
%\begin{align*}
%h\cons \valueq{\p_1}{\q_1}{\anyv_1} \cons \valueq{\p_2}{\q_2}{\anyv_2}  \cons h'
%\equivq 
%\qquad \qquad \qquad
%\\
%%\vspace{5mm}
%\qquad \qquad \qquad
%h\cons \valueq{\p_2}{\q_2}{\anyv_2} \cons \valueq{\p_1}{\q_1}{\anyv_1} \cons h'
%\end{align*}
%whenever $\p_1 \neq \p_2 \land \q_1 \neq \q_2$.
%Equivalence $\equivq$ extends  to configurations as expected.
%\end{definition}
%%% ==== END QUEUE EQUIVALENCE

\added{Abstraction passing can implement a form of \emph{session delegation}, for 
received abstractions $\abs{x}{P}$ can contain 
 free session names (indexed by participant identities). The following definition  identifies those names:}

\begin{definition}
Let 
$h$ and $\p$ be a queue 
and a participant, respectively. 
Also, let  
$\{\valueq{\q_1}{\p}{\abs{x_1}{P_1}}, \ldots, \valueq{\q_k}{\p}{\abs{x_k}{P_k}} \}$ 
 denote the (possibly empty) set of messages in $h$ containing abstractions sent to $\p$.
We write 
$\names{\p, h}$ to denote the set of participant identities occurring in 
$P_1, \ldots, P_k$.
%$\sn{P_1} \cup \cdots \cup \sn{P_k}$.}
\end{definition}
\input{semdec}
%\noindent 
The reduction relation $\red$ is defined as the union of two relations: 
the forward and backward
reduction relations, denoted $\fw$  and $\bk$, respectively. That is, $\red = \fw \cup \bk$. Relations $\fw$ and 
$\bk$ are the smallest evaluation-closed relations satisfying the rules in Figs.~\ref{fig:fw} and~\ref{fig:bk}. We indicate with $ \trans{\red} $, $ \fws $, and $ \bks $  the reflexive and transitive closure of $\red$, $\fw$ and $\bk$, respectively.
%We write $M \red^k M'$ to denote a sequence of $k \geq 0$ reduction steps (if $k=0$ then $M = M'$)
We now discuss the forward reduction rules (Fig.~\ref{fig:fw}), omitting empty tags $\normark$:
% given in \ref{fig:fw} and \ref{fig:bk}.

\begin{enumerate}[$\fwcolor{\blacktriangleright}$]
\item Rule \fwcolor{\textsc{(Init)}} initiates a choreography  $G$ with $n$ participants.
Given the composition of one service request and $n-1$ service accepts (all along $a$, available in different locations~$\loc_i$),
this rule sets up the run-time elements:
running processes and  monitors---one for each participant, with empty tag (omitted)---and the empty session queue. 
A unique session identifier  ($s$ in the rule) is also created.
The processes are inserted in 
their respective running structures, and instantiated with an appropriate session name.
Similarly, the local types for each participant are inserted in their respective monitor, with the cursor $\past$ at the beginning.

\item Rule \fwcolor{\textsc{(Out)}} starts the output of value $V$ from $\p$ to $\q$. Given an output-prefixed process as running process,
and a monitor with a local type supporting an output action, reduction adds the message $\valueq{\p}{\q}{\myeval{V}{\sigma}}$ to the output part of the session queue (where $\sigma$ is the current store). Also, the cursor within the local type is moved accordingly.
In this rule (but also in several other rules), premise $\p = \er \,\vee\, \p \in \names{\er, h_i}$ allows performing actions on names previously received via abstraction passing.

\item Rule \fwcolor{\textsc{(In)}} allows a participant $\p$ to receive a value $V$ from $\q$: it 
simply takes the first element of the output part of the queue and places it in the input part.
The cursor of the local type and state in the  monitor for $\p$ are updated accordingly.

\item Rule \fwcolor{\textsc{(Sel)}} is the forward rule for labeled selection, which in our case entails a non-deterministic choice between 
pairwise different labels indexed by $I$. %This is how our construct is more general than usual selection constructs.
We require that $I$ is contained in $J$, i.e., the set that indexes the choice according to the choreography. 
After reduction, the selected label ($\lbl_w$ in the rule) is added to the output part of the queue, and the continuation $P_w$ is kept in the running process;
to support reversibility,
alternatives different from $\lbl_w$ are stored in the stack $\stack{C}$ with their continuations.
The cursor is also appropriately updated in the  monitor.

\item Rule~\fwcolor{\textsc{(Bra)}} is similar to Rule \fwcolor{\textsc{(Sel)}}: it takes a message containing a label $\lbl_w$ as the first element in the output part of the queue, and places it into the input part. This entails a selection between the options indexed by $I$; the continuation $P_w$ is kept in the running process, and all those options different from $\lbl_w$ are kept in the stack. Also, the local type in the monitor is updated accordingly.

\item Rule~\fwcolor{\textsc{(Beta)}} handles name applications. Reduction  creates a fresh identifier ($k$ in the rule) for the running function, which keeps (i) the structure of the process prior to application, and (ii) the identifier of the running process that ``invokes'' the application. Notice that $k$ is recorded also in the monitor: this is necessary to undo applications in the proper order. To determine the actual abstraction and the name applied, we use   $\store$.

\item Rule~\fwcolor{\textsc{(Spawn)}} handles parallel composition. Location $\loc$ is ``split'' into running processes with fresh identifiers ($\loc_1, \loc_2$ in the rule). This split is recorded in the   monitor.
\end{enumerate}

\noindent
Now we comment on the backward rules (Fig.~\ref{fig:bk}) which, in most cases, change the monitor tags from $\normark$ into $\bkcolor{\rmark}$:

\begin{enumerate}[$\bkcolor{\blacktriangleleft}$]
\item Rule \bkcolor{\textsc{(RInit)}} undoes session establishment. It requires that local types for every participant are at the beginning of the protocol, and empty session queue and process stacks. Run-time elements are discarded; located service accept/requests are reinstated.

\item Rule~\bkcolor{\textsc{(RollS)}} starts to undo an input-output synchronization between $\p$ and $\q$. 
Enabled when there are complementary session types in the two monitors, this rule changes the monitor tags  from $\normark$ to $\bkcolor{\rmark}$. %, and marks  the queue with $\p$ and $\q$, to indicate that messages in the queue could now be moved between its input and output parts. 
This way, the undoing of input and output actions occurs in a decoupled way. 
%\item 
Rule \bkcolor{\textsc{(RollC)}} is the analog of~\bkcolor{\textsc{(RollS)}} but for synchronizations originated in labeled choices.

\item Rule \bkcolor{\textsc{(ROut)}} undoes an output. This is only possible for a  monitor tagged with $\bkcolor{\rmark}$, exploiting the first message in the input queue. After reduction, the process prefix is reinstated, the cursor is adjusted, the message is removed from the queue, 
the   monitor is tagged again with $\normark$.
%, and the identity of the involved participant ($\p$ in the rule) is removed from the  queue
%\item 
Rule \bkcolor{\textsc{(RIn)}} is the analog of Rule \bkcolor{\textsc{(ROut)}}. In this case, we also need to update the state of store $\store$. 
%\jp{Actually, it seems better to explain \textsc{(RollIn)} first and then \textsc{(RollOut)}.}

\item Rule \bkcolor{\textsc{(RBra)}} undoes the input part of a labeled choice: the choice context is reinstated; the cursor is moved; the last message in the input part of the queue is moved to the output part. 
%; the identity of the participant ($\p$ in the rule) is removed from the queue; and the monitor is tagged again with $\normark$.
%\item 
Rule \bkcolor{\textsc{(RSel)}} is the analog of~\bkcolor{\textsc{(RBra)}}, but for the output part of the labeled choice. The non-deterministic   selection is reinstated.

\item Rule \bkcolor{\textsc{(RBeta)}} undoes $\beta$-reduction, reinstating the application. The running function disappears, using the information in the 
  monitor ($k$ in the rule).
Rule~\bkcolor{\textsc{(RSpawn)}} undoes the spawn of a parallel thread, using the identifiers in the  monitor. 
%\jp{This rule will depend on what we decide for parallel inside processes, and session initiation.}
\end{enumerate}

\noindent
We now illustrate our reversible process model with an example.

\section{Example: the Three-Buyer protocol}
\label{s:examp}
We illustrate our  framework by presenting a reversible variant of the \emph{Three-Buyer protocol}   (see, e.g.,~\cite{CDYP2015})
with abstraction passing (code mobility), one of the 
distinctive traits of our framework. 
(In App.~\ref{app:choices} we discuss an additional example involving labeled choices.)

The protocol 
involves three buyers---Alice ($\pA$), Bob ($\pB$), and Carol ($\pC$)---who interact with a Seller ($\pS$) as follows:

\begin{enumerate}[1.]
\item 
Alice sends a book title to Seller, which replies back to Alice and Bob with a quote. Alice tells Bob how much she can contribute.
\item Bob notifies Seller and Alice that he agrees with the price, and asks Carol to assist him in completing the protocol. 
To delegate his remaining interactions with Alice and Seller to Carol, Bob sends her %both an endpoint and 
the code she must execute.
\item Carol continues the rest of the protocol with Seller and Alice as if she were Bob. 
She sends Bob's address (contained in the mobile code she received) to Seller.
\item Seller answers to Alice and Carol (who represents Bob) with the delivery date.
\end{enumerate}

%\newpage

We formalize this protocol is 
as the global type $G$ below.
%, another one involving Bob and Carol ($G_2$).
We write
$\gtcom{\p}{\{\q_1,\q_2\}}{U}{G}$
as a shorthand notation for 
$\gtcom{\p}{\q_1}{U}{\gtcom{\p}{\q_2}{U}{G}}$
(and similarly for local types).
We write $\thunkt$ to denote the type $\shot{\lend}$, associated to a \emph{thunk process} $\abs{x}{P}$ with $x \not \in \fn{P}$, written
$\thunkp{P}$. A thunk is an inactive process; it can be activated by applying to it a dummy name of type $\lend$, denoted $\dummyn$.
This way, we have 
$(\appl{\thunkp{P}}{\dummyn}) \fw P$.
\begin{align*}
G = ~&  \gtcom{A}{S}{\mathsf{title}}{\gtcom{S}{\{A,B\}}{\mathsf{price}}{\gtcom{A}{B}{\mathsf{share}}{
\\
& \quad \gtcom{B}{\{A,S\}}{\mathsf{OK}}{
\\
& \quad \gtcom{B}{C}{\mathsf{share}}{\gtcom{B}{C}{\thunkt}{
\\
& \quad \gtcom{B}{S}{\mathsf{address}}{\gtcom{S}{B}{\mathsf{date}}{\gend}}}}}}}}
%\\
%G_2 = ~& \gtcom{B}{C}{\mathsf{share}}{\gtcom{B}{C}{T}{\gtcom{B}{C}{\shot{T}}{\gend}}}
\end{align*}
%where $T = \ltout{S}{\mathsf{address}}{\ltinp{S}{\mathsf{date}}{\lend}}$ is the protocol that Bob delegates to Carol.
where  $\mathsf{price}$ and $\mathsf{share}$ are base types treated as integers,
and $\mathsf{title}$, $\mathsf{OK}$, $\mathsf{address}$, and $\mathsf{date}$ are base types treated as strings.

Then we have the following projections of $G$ onto local types:
\begin{align*}
\tproj{G}{\pS} & = \ltinp{A}{\mathsf{title}}{\ltout{\{A,B\}}{\mathsf{price}}{\ltinp{B}{\mathsf{OK}}{\ltinp{B}{\mathsf{address}}{\ltout{B}{\mathsf{date}}{\lend}}}}}
\\
\tproj{G}{\pA} & = \ltout{S}{\mathsf{title}}{\ltinp{S}{\mathsf{price}}{\ltout{B}{\mathsf{share}}{\ltinp{B}{\mathsf{OK}}{\lend}}}}
\\
\tproj{G}{\pB} & = \ltinp{S}{\mathsf{price}}{\ltinp{A}{\mathsf{share}}{\ltout{\{A,S\}}{\mathsf{OK}}{
\ltout{C}{\mathsf{share}}{\ltout{C}{\thunkt}{
\\
& \qquad \ltout{S}{\mathsf{address}}{\ltinp{S}{\mathsf{date}}{\lend}}}}}}}
\\
\tproj{G}{\pC} & = \ltinp{B}{\mathsf{share}}{\ltinp{B}{\thunkt}{\lend}}
\end{align*}
We now give processes for each participant:
\begin{align*}
\text{Seller} & =  \bout{d}{x:\tproj{G}{\pS}}\binp{x}{t}\bout{x}{price(t)}\bout{x}{price(t)}\\
& \qquad \binp{x}{ok}\binp{x}{a} \bout{x}{date}\inact  
\\
\text{Alice} & =  \binp{d}{y:\tproj{G}{\pA}}\bout{y}{\exBook}\binp{y}{p}\binp{y}{s}\binp{y}{ok}\inact  
\\
\text{Bob} & =  \binp{d}{z:\tproj{G}{\pB}}\binp{z}{p}\binp{z}{s}\bout{z}{ok}\bout{z}{ok}\bout{z}{s}
  \\
  & \qquad \qquad \bbout{z}{\thunkp{\bout{z}{\text{`Lucca, 55100'}}\binp{z}{d}\inact}}\inact
  \\
\text{Carol} & =  \binp{d}{w:\tproj{G}{\pC}}\binp{w}{s}\binp{w}{code}(\appl{code}{\dummyn})
%&Q_B = \bout{y}{share}\bout{y}{T}\bout{y}{R}\inact  \\
%&Q_C = \binp{y}{share}\binp{y}{T}\binp{y}{X}\inact  \\
\end{align*}
where $price(\cdot)$ returns a value of type $\mathsf{price}$ given a $\mathsf{title}$.
Observe how Bob's implementation sends part of its protocol to Carol in the form of a thunk containing 
his session name and address. This is how abstraction passing may serve to implement session delegation.

The whole system, given by configuration $M$ below, is obtained by placing these process implementations in appropriate locations:
$$
M = \myloc{\loc_1}{\text{Seller}} 
\Par
\myloc{\loc_2}{\text{Alice}} 
\Par
\myloc{\loc_3}{\text{Bob}} 
\Par 
\myloc{\loc_4}{\text{Carol}} 
$$

The session starts with an application of 
Rule \fwcolor{\textsc{(Init)}}:
%To simplify readability, below
%we write 
%$\mathtt{r}$,
%$\mathtt{a}$,
%$\mathtt{b}$,
%and 
%$\mathtt{c}$ 
%instead of participant identities $\mathsf{S}$, $\mathsf{A}$, $\mathsf{B}$, and $\mathsf{C}$, respectively:
%$$
\begin{align*}
%\begin{array}{cc}
M & \fw  \news{s}\big(\, 
\np{\key{\loc_1}{\pS}}{ \conf{\inact}{S_1\subst{\epS}{x}}} \Par 
\hmoni{s_{\pS}}{\past \tproj{G}{\mathsf{S}}}{x}{\upd{x}{d}}  
\\
& \Par \np{\key{\loc_2}{\pA}}{ \conf{\inact}{A_1\subst{\epA}{y}}} \Par 
\hmoni{s_\pA}{\past \tproj{G}{\mathsf{A}}}{y}{\upd{y}{d}} 
\\
& \Par \np{\key{\loc_3}{\pB}}{ \conf{\inact}{B_1\subst{\epB}{z}}} \Par 
\hmoni{s_\pB}{\past \tproj{G}{\mathsf{B}}}{z}{\upd{z}{d}} 
\\
& \Par \np{\key{\loc_4}{\pC}}{ \conf{\inact}{C_1\subst{\epC}{w}}} \Par 
\hmoni{s_\pC}{\past \tproj{G}{\mathsf{C}}}{w}{\upd{w}{d}}  
\\
& \Par \codah{s}{\emp}{\emp}{}~\big)  = M_1
%\end{array}
\end{align*}
%$$
where 
$S_1$, $A_1$, $B_1$, and $C_1$ 
stand for the continuation of processes $\text{Seller}$, $\text{Alice}$, $\text{Bob}$, and $\text{Carol}$ after the service 
request/declaration. So, e.g., 
$
A_1 = \bout{y}{\exBook}\binp{y}{p}\binp{y}{s}\binp{y}{ok}\inact
$.
We use configuration $M_1$ to illustrate some forward and backward reductions.

From $M_1$ we could either undo the reduction (using Rule~\bkcolor{\textsc{(RInit)}})
or execute the communication from $\text{Alice}$ to $\text{Seller}$ (using two rules:~\fwcolor{\textsc{(Out)}} and ~\fwcolor{\textsc{(In)}}). This latter option would be as follows:
\begin{align*}
M_1 & \fw  \news{s}(\,  \np{\key{\loc_2}{\pA}}{ \conf{\inact}{\binp{\epA}{p}\binp{\epA}{s}\binp{\epA}{ok}\inact}} 
\\
& \Par 
\hmoni{s_\pA}{\ltout{S}{\mathsf{title}}{\past \ltinp{S}{\mathsf{price}}{\ltout{B}{\mathsf{share}}{\ltinp{B}{\mathsf{OK}}{\lend}}}}}{y}{\upd{y}{d}} 
\\
& \Par N_2 \Par \codah{s}{\emp}{\valueq{\pA}{\pS}{\exBook}}{}~)  = M_2
\end{align*}
where $N_2$ stands for the running processes and monitors for Seller, Bob, and Carol, not involved in the reduction.
We now have:
\begin{align*}
M_2 \fw & \news{s}(\,  \np{\key{\loc_1}{\pS}}{ \conf{\inact}{\bout{\epS}{price(t)} \bout{\epS}{price(t)}\binp{\epS}{ok}\\ 
& \qquad  \binp{\epS}{a} \bout{\epS}{date}\inact }} 
\\
& \Par 
\hmoni{s_{\pS}}{\ltinp{A}{\mathsf{title}}{\past \ltout{\{A,B\}}{\mathsf{price}}{T_\pS}}}{x,t}{\store_3}  \Par N_3
\\
&  \Par \codah{s}{\valueq{\pA}{\pS}{\exBook}}{\emp}{}~)  = M_3
\end{align*}
where 
$\store_3  = \upd{x}{d},\upd{t}{\exBook}$ is
the resulting store,
$T_\mathsf{S}  = \ltinp{B}{\mathsf{OK}}{\ltinp{B}{\mathsf{address}}{\ltout{B}{\mathsf{date}}{\lend}}}$,
and $N_3$ stands for the participants not involved in the reduction.
Observe that the cursors in monitors $s_\pS$ and $s_\pA$ have evolved, and that message from $\pA$ to $\pS$ has now been moved to the input queue.

We illustrate  reversibility by showing how to return to $M_1$ starting from $M_3$.
We need to apply three rules: \bkcolor{\textsc{(RollS)}}, \bkcolor{\textsc{(RIn)}}, and \bkcolor{\textsc{(ROut)}}.
Reversibility is decoupled in the sense that there is no fixed order in which the latter two rules should be applied; below we give just a possible sequence.
First, Rule~\bkcolor{\textsc{(RollS)}} modifies the tags of monitors $s_\pS$ and $s_\pA$,
  leaving the rest unchanged:
\begin{align*}
M_3 & \bk  \news{s}(\,  
\np{\key{\loc_1}{\pS}}{ \conf{\inact}{\bout{\epS}{price(t)}\bout{\epS}{price(t)}\binp{\epS}{ok} \\ 
& \quad  \binp{\epS}{a} \bout{\epS}{date}\inact }} 
\\
& \Par 
 \monir{s_\pS}{\ltinp{A}{\mathsf{title}}{\past \ltout{\{A,B\}}{\mathsf{price}}{T_\mathsf{B}}}}{x,t}{\store_3} 
\\
& \Par \np{\key{\loc_2}{\pA}}{ \conf{\inact}{\binp{\epA}{p}\binp{\epA}{s}\binp{\epA}{ok}\inact}} 
\\
& \Par 
\monir{s_\pA}{\ltout{S}{\mathsf{title}}{\past \ltinp{S}{\mathsf{price}}{\ltout{B}{\mathsf{share}}{\ltinp{B}{\mathsf{OK}}{\lend}}}}}{y}{\upd{y}{d}} 
\\
& \Par N_4 \Par \codah{s}{\valueq{\pA}{\pS}{\exBook}}{\emp}{}~)  = M_4
\end{align*}
where, as before, $N_4$ represents participants not involved in the reduction.
$M_4$ has several possible forward and backward reductions. 
One particular reduction uses Rule~\bkcolor{\textsc{(RIn)}}
to undo the input at \pS:
\begin{align*}
M_4 & \bk  \news{s}(\,  
\np{\key{\loc_1}{\pS}}{ \conf{\inact}{\binp{\epS}{t}\bout{\epS}{price(t)}\bout{\epS}{price(t)} \\ 
& \quad  \binp{\epS}{ok}\binp{\epS}{a} \bout{\epS}{date}\inact }} 
\\
& \Par 
 \hmoni{s_\pS}{\past \ltinp{A}{\mathsf{title}}{\ltout{\{A,B\}}{\mathsf{price}}{T_\mathsf{B}}}}{x}{\upd{x}{d}} 
\\
& \Par \np{\key{\loc_2}{\pA}}{ \conf{\inact}{\binp{\epA}{p}\binp{\epA}{s}\binp{\epA}{ok}\inact}} 
\\
& \Par 
\monir{s_\pA}{\ltout{S}{\mathsf{title}}{\past \ltinp{S}{\mathsf{price}}{\ltout{B}{\mathsf{share}}{\ltinp{B}{\mathsf{OK}}{\lend}}}}}{y}{\upd{y}{d}} 
\\
& \Par N_4 \Par \codah{s}{\emp}{\valueq{\pA}{\pS}{\exBook}}{}~)  = M_5
\end{align*}
Just as an application of Rule~\bkcolor{\textsc{(RollS)}} need not be immediately followed by 
an application of Rule~\bkcolor{\textsc{(RIn)}}, an application of Rule~\bkcolor{\textsc{(RIn)}} need not be immediately followed
by an application of Rule~\bkcolor{\textsc{(ROut)}}. A particular reduction from $M_5$ undoes the output at \pA:
\begin{align*}
M_5 & \bk  \news{s}(\,  
\np{\key{\loc_1}{\pS}}{ \conf{\inact}{\binp{\epS}{t}\bout{\epS}{price(t)}\bout{\epS}{price(t)} \\ 
& \quad  \binp{\epS}{ok}\binp{\epS}{a} \bout{\epS}{date}\inact }} 
\\
& \Par 
 \hmoni{s_\pS}{\past \ltinp{A}{\mathsf{title}}{\ltout{\{A,B\}}{\mathsf{price}}{T_\mathsf{B}}}}{x}{\upd{x}{d}} 
\\
& \Par \np{\key{\loc_2}{\pA}}{ \conf{\inact}{\bout{\epA}{\exBook}\binp{\epA}{p}\binp{\epA}{s}\binp{\epA}{ok}\inact}} 
\\
& \Par 
\hmoni{s_\pA}{\past \ltout{S}{\mathsf{title}}{\ltinp{S}{\mathsf{price}}{\ltout{B}{\mathsf{share}}{\ltinp{B}{\mathsf{OK}}{\lend}}}}}{y}{\upd{y}{d}} 
\\
& \Par N_4 \Par \codah{s}{\emp}{\emp}{}~)  = M_6
\end{align*}
Clearly, $M_6 = M_1$.
Summing up, the synchronization realized by the (forward) reduction sequence
$M_1 \fw M_2 \fw M_3$ can be reversed by the (backward) reduction sequence
$M_3 \bk M_4 \bk M_5 \bk M_6$.

To illustrate abstraction passing, let us assume that 
$M_3$ above follows a sequence of forward reductions
until the configuration:
\begin{align*}
M_7 = ~ &   \news{s}(\,  \np{\key{\loc_3}{\pB}}{ \conf{\inact}{\bbout{\epB}{\thunkp{\bout{\epB}{\text{`Lucca, 55100'}}\binp{\epB}{d}\inact}}\inact}} 
\\
& \Par \hmoni{s_\pB}{\myctxr{\ctx{T}_7}{\past \ltout{C}{\thunkt}{\ltout{S}{\mathsf{address}}{\ltinp{S}{\mathsf{date}}{\lend}}}}}{z,p,s}{\store_7} 
\\
& \Par \np{\key{\loc_4}{\pC}}{ \conf{\inact}{\binp{\epC}{code}(\appl{code}{\dummyn})}} 
\\
& \Par 
\hmoni{s_\pC}{\myctxr{\ctx{T}_8}{\past \ltinp{B}{\thunkt}{\lend}}}{w,s}{\store_8} 
\Par N_5 \Par \codah{s}{h_7}{\emp}{}~) 
\end{align*}
where 
$120 < price(\exBook)$ is the amount \pB may contribute
and
$\myctxr{\ctx{T}_7}{\bullet}$, $\store_7$, $\myctxr{\ctx{T}_8}{\bullet}$, $\store_8$,
and $h_7$ capture past interactions as follows:
\begin{align*}
\myctxr{\ctx{T}_7}{\bullet} & =
\ltinp{S}{\mathsf{price}}{\ltinp{A}{\mathsf{share}}{\ltout{\{A,S\}}{\mathsf{OK}}{
\ltout{C}{\mathsf{share}}{\bullet}}}}
\\
\store_7 & = \upd{z}{d},\upd{p}{price(\exBook)},\upd{s}{120}
\\
\myctxr{\ctx{T}_8}{\bullet} & =\ltinp{B}{\mathsf{share}}{\bullet} \qquad \store_8  = \upd{w}{d},\upd{s}{120}
\\
h_7 & = 
\valueq{\pA}{\pS}{\exBook}
\\
& \cons
\valueq{\pS}{\pA}{price(\exBook)}
\cons
\valueq{\pS}{\pB}{price(\exBook)}
\\
& \cons
\valueq{\pA}{\pB}{120}
\cons
\valueq{\pB}{\pA}{\text{`ok'}}
\cons
\valueq{\pB}{\pS}{\text{`ok'}}
\cons
\valueq{\pB}{\pC}{120}
\end{align*}
If $M_7 \fw \fw M_8$ by using Rules~\fwcolor{\textsc{(Out)}} and ~\fwcolor{\textsc{(In)}}
we would have:
\begin{align*}
M_8 & = ~   \news{s}(\,  \np{\key{\loc_3}{\pB}}{ \conf{\inact}{\inact}} 
\\
& \Par \hmoni{s_\pB}{\myctxr{\ctx{T}_7}{\ltout{C}{\thunkt}{\past\ltout{S}{\mathsf{address}}{\ltinp{S}{\mathsf{date}}{\lend}}}}}{z,p,s}{\store_7} 
\\
& \Par \np{\key{\loc_4}{\pC}}{ \conf{\inact}{(\appl{code}{\dummyn}) }} 
\\
& \Par 
\hmoni{s_\pC}{\myctxr{\ctx{T}_8}{ \ltinp{B}{\thunkt}{\past\lend}}}{w,s,code}{\store_9} 
\\
& 
\Par N_5 \Par \codah{s}{h_7 \cons \valueq{\pB}{\pC}{\thunkp{\bout{\epB}{\text{`Lucca, 55100'}}\binp{\epB}{d}\inact}}}{\emp}{}~) 
\end{align*}
where
$\store_9 = \store_8 \upd{code}{\thunkp{\bout{\epB}{\text{`Lucca, 55100'}}\binp{\epB}{d}\inact}}$.
We now may apply Rule~\fwcolor{\textsc{(Beta)}} so as to obtain:
\begin{align*}
M_8 & \fw ~   \news{s}\news{k}(\,  
%\np{\key{\loc_3}{\pB}}{ \conf{\inact}{\inact}} 
%\\
%& \Par \hmoni{s_\pB}{\myctxr{\ctx{T}_7}{\ltout{C}{\thunkt}{\past\ltout{S}{\mathsf{address}}{\ltinp{S}{\mathsf{date}}{\lend}}}}}{z,p,s}{\store_7} 
%\\
%& \Par 
\np{\key{\loc_4}{\pC}}{\conf{\inact}{\bout{\epB}{\text{`Lucca, 55100'}}\binp{\epB}{d}\inact}} 
\!\!  \Par N_6 
\\
& \!\!\Par 
\mem{k}{(\appl{code}{\dummyn})}{\loc_4} 
\Par 
\hmoni{s_\pC}{\myctxr{\ctx{T}_8}{ \ltinp{B}{\thunkt}{k.\past\lend}}}{w,s,code}{\store_9} 
\\
& 
\!\!\Par \codah{s}{h_7 \cons \valueq{\pB}{\pC}{\thunkp{\bout{\epB}{\text{`Lucca, 55100'}}\binp{\epB}{d}\inact}}}{\emp}{}~) 
= M_9
\end{align*}
where $N_6$ is for the rest of the system. 
Notice that this reduction has added a running function on a fresh 
$k$. This fresh $k$ is also used within the type stored in the monitor $s_\pC$.

The reduction $M_8 \fw M_9$ completes the code mobility from $\pB$ to $\pC$: the now active thunk
will execute $\pB$'s implementation from $\pC$'s location.
This justifies the premise 
$\p = \er \,\vee\, \p \in \names{\er, h_i}$ present in Rules~\fwcolor{\textsc{(Out)}}, \fwcolor{\textsc{(In)}}, \fwcolor{\textsc{(Sel)}} and ~\fwcolor{\textsc{(Bra)}} (and in their backward counterparts):
when executing previously received mobile code, the participant mentioned in the location (i.e., $\pC$)
and that mentioned in the located process (i.e., $\pB$) may differ.
Further forward reductions from $M_9$ will  modify the cursor in the type stored in monitor $s_\pB$
based on the process behavior located at $\key{\loc_4}{\pC}$.

\smallskip

Having introduced our process model and its reversible semantics,
 we now move on to establish its key properties.
 

\section{Main Results}
\label{s:res}

%\begin{definition}[Normal form]
%Given a reachable configuration $M$, we then have
%\end{definition}
We now establish our main result: 
we prove that reversibility in our model of choreographic, asynchronous communication is 
\emph{causally consistent}. 
%This is significant, because to our knowledge all prior work on reversible, concurrent models address the (simpler) case of synchronous communication. 
We proceed in three steps:
\begin{enumerate}[a)]
\item First, we introduce an alternative \emph{atomic}  semantics and show that it corresponds, in a tight technical sense, to the decoupled semantics in \S\,\ref{ss:semconf} (Theorems~\ref{theo:correspond} and \ref{t:bf}). 
\item Second, in the light of this correspondence, we establish causal consistency for the atomic semantics, following the  approach of Danos and Krivine~\cite{DBLP:conf/concur/DanosK05} (Theorem~\ref{t:causal}).
\item Finally, we state a fine-grained, bidirectional connection between the semantics of (high-level) global types with the decoupled semantics of  (low-level) configurations (Theorem~\ref{t:corrgc}). 
\end{enumerate}
As a  result of these  steps, we may 
transfer causal consistency to choreographies expressed as global types.
%\jp{Perhaps it is more logical to relate global types and configurations first (3.3 moved forward)?}

\subsection{Atomic Semantics vs. Decoupled Semantics}\label{sec:atom}
\input{sematom}


\subsection{Causal Consistency}

 Theorems~\ref{theo:correspond} and~\ref{t:bf} allow us to focus on the atomic reduction $\reda$  for the purposes of establishing causal consistency. 
We adapt the approach of~\cite{DBLP:conf/concur/DanosK05} (developed for a reversible CCS) to our  
 higher-order session $\pi$-calculus with asynchronous   communication.
Causal consistency concerns traces of \emph{transitions}:
\begin{definition}
A \emph{transition} $t$ is a triplet of the form
$t : M\lreda{\memstamp}N$ where $M\reda N$ and 
the \emph{transition stamp}
$\memstamp$ is defined as follows:
\begin{enumerate}[$\bullet$]
	\item $\memstamp = \{ \loc_1,\cdots,\loc_n \}$, if  Rule~\fwcolor{(\textsc{Init})} or~\fwcolor{(\textsc{RInit})}  is used;
	\item $\memstamp = \{ \p,\q \}$, if one of Rules~\fwcolor{(\textsc{AC})}, \fwcolor{(\textsc{AS})}, \bkcolor{(\textsc{RAC})} and \bkcolor{(\textsc{RAS})} is used;
	\item $\memstamp = \{ \loc, \p \}$, if one of Rules~\fwcolor{(\textsc{Beta})}, \fwcolor{(\textsc{Spawn})}, 
	\bkcolor{(\textsc{RBeta})} or \bkcolor{(\textsc{RSpawn})} is used.
\end{enumerate} 
\end{definition}
\noindent
%Some terminology on transitions is in order.
Given $t : M\lfwa{\memstamp}N$, we say 
$M$ 
and $N$ are its
source 
and target
(written $\tsource{t}$ and $\ttarget{t}$), respectively. % and $N$ is the target of $t$ (written ). 
A transition
$t : M\lreda{\memstamp}N$ is \textit{forward} if $M\fwa N$ and \textit{backward} if $M\bka N$. 
Given $t:M\lreda{\memstamp}N$, 
its \emph{inverse}, denoted $\nottrace{t}$, is the transition $\nottrace{t}:N\lreda{\memstamp}M$.
Two transitions are  \emph{coinitial} if they have the same source; 
\emph{cofinal} if they have the same target;
\emph{composable} if the target of the first one is the source of the other. 
Given coinitial transitions $t_1 : M \lreda{\memstamp_1} N_1$ and 
$t_2 : M \lreda{\memstamp_2} N_2$, we define $t_2/t_1$ (read ``$t_2$ after $t_1$'') as 
$N_1\lreda{\memstamp_2} N_2$, i.e., the transition with stamp $\memstamp_2$ that starts from the target of $t_1$.
A \emph{trace} is a sequence of pairwise composable transitions. 
We let $t$ and $\trace$ %(their decorated variants) 
range over transitions and traces, respectively. 
Notions of target, source, composability and inverse extend naturally to traces. 
We write $\etrace_M$ to denote the empty trace with source $M$, 
and $\trace_1;\trace_2$ to denote the composition of two composable traces $\trace_1$ and $\trace_2$. 
%The stamp ?(m ) of a memory m = [?1 : a?P? | ?2 : a(X) ? Q ;k] is defined to be the set {?1,?2,k}; we set ?(m ) = ?(m ).
Two important classes of transitions are \emph{conflicting} and \emph{concurrent} ones:

\begin{definition}%[Conflicting and Concurrent Transitions]
Two coinitial transitions $t_1: M\lreda{\memstamp_1} M_1$ and 
$t_2: M\lreda{\memstamp_2} M_2$ are said to be in \emph{conflict} if
$\memstamp_1 \cap \memstamp_2 \neq 0$. 
Two transitions are  \emph{concurrent} if they are not in conflict.
\end{definition}
\noindent
A property that a reversible semantics should enjoy is the so-called Square Lemma~\cite{DBLP:conf/concur/DanosK05}, which may be informally described as follows. Assume a configuration from which two transitions are possible: if these transitions are concurrent then the order in which they are executed does not matter, and the same configuration is reached. %Formally we have: 
\begin{lemma}[Square]\label{lemma:square}
If $t_1: M\lreda{\memstamp_1} M_1$ and $t_2: M\lreda{\memstamp_2} M_2$ are coinitial and concurrent transitions, then there exist cofinal transitions $t_2/t_1= M_1 \lreda{\memstamp_2} N$ and
$t_1/t_2= M_2 \lreda{\memstamp_1} N$.
\end{lemma}
\noindent
%We are now in a position to show that our reversible semantics $\reda$ is causally consistent. We define a notion of \emph{causal equivalence}  $\causeq$ between traces, which abstracts away from the order in which concurrent reductions are executed.

\begin{definition}
We define $\causeq$ as the least equivalence between traces that is closed under composition and that obeys:
i)~$t_1; t_2/t_1 \causeq t_2; t_1/t_2$; ii)~ $t;\nottrace{t} \causeq \etrace_{\tsource{t}}$; iii)~$\nottrace{t};t \causeq \etrace_{\ttarget{t}}
$.
\end{definition}
\noindent
Intuitively, $\causeq$ says that: 
(a) given two concurrent transitions, the traces obtained by swapping their execution order are equivalent; 
(b) a trace consisting of opposing transitions is equivalent to the empty trace.
The proof of causal consistency follows that in~\cite{DBLP:conf/concur/DanosK05}, but with simpler arguments because of our simpler transition stamps. The following lemma says that, up to causal equivalence, traces can be rearranged so as to reach the maximum freedom of choice, first going only backwards, and then going only forward. 

\begin{lemma}[Rearranging]\label{lemma:rearranging}
 Let $\trace$ be a trace. There are forward traces $\trace', \trace''$ such that 
 $\trace \causeq \nottrace{ \trace' }; \trace''$.
\end{lemma}
\begin{proof}
 By lexicographic induction on the length of $\trace$ and on the distance between the beginning of 
$\trace$ and the earliest pair of opposing transitions in $\trace$. The analysis uses both the Loop Lemma 
(Lemma~\ref{lemma:loop}) and the Square Lemma (Lemma~\ref{lemma:square}).
\end{proof}

\noindent
%We now consider the following situation: if 
If trace $\trace_1$ and forward trace 
$\trace_2$ start from the same configuration and end up in the same configuration, then $\trace_1$ may contain some ``local steps'', not present in $\trace_2$, which must be eventually reversed---otherwise there would be a difference with respect to   $\trace_2$. 
Hence, $\trace_1$ could be \emph{shortened} by removing such local steps and their corresponding reverse steps. 
\begin{lemma}[Shortening]\label{lemma:shortening}
 Let $\trace_1, \trace_2$ be coinitial and cofinal traces, 
 with $\trace_2$ forward. Then, there exists a forward trace 
 $\trace'_1$ of length at most that of $\trace_1$ such that 
 $\trace'_1 \causeq \trace_1$.
\end{lemma}
\begin{proof}
By induction on the length of $\trace_1$, using Square and Rearranging Lemmas (Lemmas~\ref{lemma:square},~\ref{lemma:rearranging}). 
The proof uses the forward trace $\trace_2$ as guideline for shortening $\trace_1$ into a forward trace, relying  on the fact that $\trace_1, \trace_2$ share the same source and target.
\end{proof}
We may now state our main result:
\begin{theorem}[Causal consistency]\label{t:causal}
 Let $\trace_1$ and $\trace_2$ be coinitial traces, then 
 $\trace_1 \causeq \trace_2$ if and only if $\trace_1$ and $\trace_2$ are cofinal.
\end{theorem}
\begin{proof}
The `if' direction follows by definition of $\causeq$ and trace composition. The `only if' direction uses Square, Rearranging and Shortening Lemmas (Lemmas~\ref{lemma:square},~\ref{lemma:rearranging},~\ref{lemma:shortening}). 
\end{proof}

\subsection{Connecting (Reversible) Choreographies and (Reversible) Configurations}\label{ss:conn}
We now relate choreographies and configurations to connect the two levels of abstraction for reversible global protocols.
\added{For convenience, we focus on first-order global types (i.e., without abstraction passing), relying 
on a simple characterization of the \emph{well-formed processes} that implement a given local type.} 
We write $\ladeq{P}{T}{x}$ to denote that $P$ implements the local type $T$ along variable $x$---see App.~\ref{app:adeq} for a  definition. We may then define the configurations that implement a global type with history. First, an auxiliary definition:

\begin{definition}
We say the global type with history $\gth{H}$ is \emph{reachable} if it can be obtained from a global type $G$
via a %(non empty) 
sequence of $\fwg$ and $\bkg$ transitions (cf. Fig.~\ref{f:gts}).
\end{definition}

\begin{definition}\label{d:ii}
Let $\gth{G}$ 
be a global type, 
with $\parties{G}= \{\p_1,\cdots,\p_n\}$.
We say that
configuration $M$  \emph{initially implements} $G$ if we have
\begin{align*}
M\equiv  
\news{s} \Big(\, 
\prod_{i \in\{1,\cdots,n\}} \np{\key{\loc_i}{\p_i}}{ \conf{\inact}{P_i\subst{\key{s}{\p_i}}{x_i}}} \Par 
\\
\moni{s_{\p_i}}{\past\tproj{G}{\p_i}}{x_i}{\store_i}  \Par \codah{s}{\epsilon}{\epsilon}\Big)
\end{align*}
with $\ladeq{P_i}{\tproj{G}{\p_i}}{x_i}$, for all $i \in\{1,\!\cdots\!,n\}$, 
for some stores $\store_1, \ldots, \store_n$.
A configuration $N$ \emph{implements} the global type with history $\gth{H}$, written $\adeq{N}{\gth{H}}$, if
there exist $M, G$ such that (i)~$\gth{H}$ is reachable from $G$, (ii) $M$ initially implements $G$, and (iii) $N$ is reachable from $M$.
\end{definition}


%\begin{definition}
%Let $\gth{H}$ 
%be a global type with history, 
%with $\parties{\gth{H}}= \{\p_1,\cdots,\p_n\}$.
%We say 
%configuration $M$  \emph{implements} $\gth{H}$ (written $\adeq{M}{\gth{H}}$) if we have
%$$
%M\equiv  
%\news{s} \Big(\, 
%\prod_{i \in\{1,\cdots,n\}} \np{\key{\loc_i}{\p_i}}{ \conf{\stack C_i}{P_i}} \Par 
%\moni{s_{\p_i}}{\myctxr{\ctx T_i}{\past\tproj{\gth{H}}{\p_i}}}{\widetilde{x_i}}{\store_i}  \Par \codah{s}{h_1}{h_2}\Big)
%$$
%with $\adeq{P_i}{\tproj{\gth{H}}{\p_i}}$, for all $i \in\{1,\!\cdots\!,n\}$, 
%for some stacks $\stack{C}_1, \ldots, \stack{C}_n$, 
%type context $\ctx T_1, \ldots, \ctx T_n$,
%sequences $\widetilde{x_1}, \ldots, \widetilde{x_n}$, 
%stores $\store_1, \ldots, \store_n$, and queues $h_1$, $h_2$.
%%\prod_{i}\myloc{\loc_i}{P_i} \Par \news{s} \big(\prod_{j}\np{\loc_j}{\conf{\stack C_j}{P_j}} \Par \prod_z
%%\moni{s_\p}{ T_z }{\mytilde x_z}{\store_z} \Par \codah{s}{h_1}{h_2} \big)$$
%\end{definition}



%, we shall appeal to a \emph{pool} of (typed) processes, denoted $\mathcal{P}$, which
%contains pairs $(P, T)$ of processes that conform to a declared local type.
%We require the following definition:
%
%\begin{definition}
%Given a global type $G$ (with $\parties{G}= \{\p_1,\cdots,\p_n\}$) and a pool $\mathcal{P}$, 
%we write
%$\impl{G}{P}$
%to denote the set of initial configurations
%%$$
%%\left\{
%%\myloc{\loc_1}{\bout{a}{x:T_1}{P_{1}}} 
%%\!\Par \!\!\!
%%\prod_{j \in \{2, \cdots, n\}}\myloc{\loc_j}{\binp{a}{x:T_j}{P_{j}}} 
%%\!\!\bnfbar\!\! 
%%\forall \gpart{p}_i\in \parties{G}. (\, \tproj{G}{\gpart{p}_i} = T_{i} \,\land\, (P_i, T_i) \in \mathcal{P})
%%\right\}
%%$$
%$$
%\left\{
%\myloc{\loc_1}{\bout{a}{x:\tproj{G}{\gpart{p}_1}}{P_{1}}} 
%\!\Par \!\!\!
%\prod_{j \in \{2, \cdots, n\}}\myloc{\loc_j}{\binp{a}{x:\tproj{G}{\gpart{p}_j}}{P_{j}}} 
%\!\!\bnfbar\!\! 
%\forall \gpart{p}_i\in \parties{G}.(P_i, \tproj{G}{\gpart{p}_i}) \in \mathcal{P}
%\right\}
%$$
%\end{definition}
%\noindent This way, given a choreography $G$, every configuration in $\impl{G}{P}$ can execute its corresponding global protocol, starting with Rule~\textsc{Init}. Thus, configurations in $\impl{G}{P}$ are one (forward) step away from actually implementing $G$.
%It is then convenient to define the set $\impll{G}{P} = \{ M \bnfbar N \fw M \,\land\, N \in \impl{G}{P}\}$ which
% collects \emph{runnable configurations}, i.e., configurations after session initiation, with initialized monitors and empty queue.
%
%A difference between choreographies and their implementations (i.e., configurations) is that the latter specify both behavior and state whereas the former only describe behavior. Therefore, to relate choreographies and configurations we abstract from the state in queues.
%Given a runnable configuration $M$, below we write $\nostate{M}$ to denote the resulting configuration after erasing the queue.
%This way, if $M$ and $M'$ are identical in all aspects excepting their associated queue, we will have that $\nostate{M} = \nostate{M'}$.

%%% ==== START SWAPPING
The last ingredient required %in giving semantics to choreographies 
is a \emph{swapping relation} over global types, denoted \swap, which enables 
behavior-preserving
transformations among causally independent communications. 
%Such transformations may represent optimizations that increase parallelism while preserving the intended global behavior.

\begin{definition}[Swapping]
We define \swap as the smallest congruence on $G$ that satisfies the rules in Fig.~\ref{f:swap}
(where we omit the symmetric of (\textsc{Sw1}), (\textsc{Sw2}), and (\textsc{Sw3})).
We extend \swap  to global types with history $\mathsf{H}$ as follows:
$\ctx{G}[\past G_1] \swap \ctx{G'}[\past G_2]$ 
if 
$\ctx{G}[\gend] \swap \ctx{G'}[\gend]$
and 
$G_1 \swap G_2$.
\end{definition}

\begin{figure}[t!]
{\small
\begin{mathpar}
\inferrule*[left=(Sw1)]{\{\p_1,\q_1\}\#\{\p_2,\q_2\}}
{
\begin{array}{c}
\gtcom{\p_1}{\q_1}{U_1}{(\gtcom{\p_2}{\q_2}{U_2}{G})}
\swap 
\\
\qquad \qquad \gtcom{\p_2}{\q_2}{U_2}{(\gtcom{\p_1}{\q_1}{U_1}{G})}
\end{array}
}
\\
\inferrule*[left=(Sw2)]{\{\p_1,\q_1\}\#\{\p_2,\q_2\}}
{
\begin{array}{c}
\gtcom{\p_1}{\q_1}{U_1}{(\gtcho{\p_2}{\q_2}{\lbl_i}{G_i})}
\swap \\
\qquad \qquad \gtcho{\p_2}{\q_2}{\lbl_i}{(\gtcom{\p_1}{\q_1}{U_1}{G_i})}
\end{array}
}
\\
\inferrule*[left=(Sw3)]{\{\p_1,\q_1\}\#\{\p_2,\q_2\}}
{
\begin{array}{c}
\gtchoi{\p_1}{\q_1}{\lbl_i}{(\gtchoi{\p_2}{\q_2}{\lbl_j}{G_j}{j \in J})}{i \in I}
\swap
\\
\qquad \qquad
\gtchoi{\p_2}{\q_2}{\lbl_j}{(\gtchoi{\p_1}{\q_1}{\lbl_i}{G_i}{i \in I})}{j \in J}
\end{array}
}
\end{mathpar}
}
\vspace{-4mm}
\caption{Swapping on global types $G$. We write $A \# B$ if $A$ and $B$ are disjoint sets.\label{f:swap}}
\end{figure}

%%% ==== END SWAPPING

%%%% ==== START QUEUE EQUIVALENCE
%\begin{definition}[Equivalence on message queues]
%%\cm{Not sure we need this, otherwise we have that $a \rightarrow b; c \rightarrow d = c \rightarrow d; a \rightarrow b$}
%%\jp{I have modified this.}
%%Let $m$ stand for either $V$ or $\lbl$. 
%We define the structural equivalence on queues, denoted $\equivq$, as follows:
%\begin{align*}
%h\cons \valueq{\p_1}{\q_1}{\anyv_1} \cons \valueq{\p_2}{\q_2}{\anyv_2}  \cons h'
%\equivq 
%\qquad \qquad \qquad
%\\
%%\vspace{5mm}
%\qquad \qquad \qquad
%h\cons \valueq{\p_2}{\q_2}{\anyv_2} \cons \valueq{\p_1}{\q_1}{\anyv_1} \cons h'
%\end{align*}
%whenever $\p_1 \neq \p_2 \land \q_1 \neq \q_2$.
%Equivalence $\equivq$ extends  to configurations as expected.
%\end{definition}
%%%% ==== END QUEUE EQUIVALENCE

\noindent We may now    relate (i)~transitions in the  semantics of (high-level) global types (with history) with 
(ii)~reductions in the  semantics of their (low-level) process implementations. We write $M \bkk M'$ to denote a sequence of $j \geq 0$ reduction steps (if $j=0$ then $M = M'$).

%\begin{theorem}\label{t:corrgc}
%Let $\mathsf{H}$  be a reachable global type with history (cf. \S\,\ref{ss:chore}).
%\begin{enumerate}[a)]
%\item If $\adeq{M}{\gth{H}}$ and $\gth{H} \fwg \gth{H}'$ (resp. $\gth{H} \bkg \gth{H}'$) then  there exists $M'$ such that $M \fw M'$ (resp. $M \bk\bk M'$) and $\adeq{M'}{\gth{H'}}$.
%\item If $\adeq{M}{\gth{H}}$ and $M \fw N$ (resp. $M \bk\bk N$) then there exists $\gth{H}'$
%such that 
% $\gth{H} \fwg \gth{H}'$ (resp. $\gth{H} \bkg \gth{H}'$) and $\adeq{N}{\gth{H'}}$.
%\end{enumerate} 
%\end{theorem}

\begin{theorem}\label{t:corrgc}
Let $\mathsf{H}$  be a reachable, first-order global type with history (cf. \S\,\ref{ss:chore}).
\begin{enumerate}[a)]
\item If $\adeq{M}{\gth{H}}$ and $\gth{H} \fwg \gth{H}'$  then  $M \fw M'$  and $\adeq{M'}{\gth{H'}}$, for some $M'$.
If $\adeq{M}{\gth{H}}$ and $\gth{H} \bkg \gth{H}'$ then $M \bkk M'$ (with $j =1$ or $j=2$) and $\adeq{M'}{\gth{H'}}$, for some $M'$.

%\item If $\adeq{M}{\gth{H}}$ and $M \fw N$ then 
% $\gth{H} \swap \gth{H}'\fwg \gth{H}''$  and $\adeq{N}{\gth{H}''}$, for some  $\gth{H}'$, $\gth{H}''$.
% If $\adeq{M}{\gth{H}}$ 
% and $M \bk N'$ then  
% $N' \bk^k N$ (with $k =0$ or $k=1$),
% $\gth{H} \swap \gth{H}' \bkg \gth{H}''$,
% and $\adeq{N}{\gth{H'}}$, for some  $N$, $\gth{H}'$, $\gth{H}''$.

\item Suppose $\adeq{M}{\gth{H}}$. For all configurations $N_i$ such that $M \fw N_i$ there exist 
$\gth{H}_i, \gth{H}'_i, \gth{H}''$,
and $M'$,
such that
 $\gth{H} \swap \gth{H}_i\fwg \gth{H}'_i$,
 $\adeq{N_i}{\gth{H}'_i}$,
 $N_i \fws M'$,
 $\gth{H}'_i \fwgs \gth{H}''$,
 and 
 $\adeq{M'}{\gth{H}''}$
 (and similarly for $\bk$, $\bkg$).

\end{enumerate} 
\end{theorem}

%\cm{Should take into account swapping}
\begin{proof}
By induction on the transitions/reductions.
See Appendix~\ref{app:corrgc} for details.
\end{proof}

Theorem~\ref{t:corrgc} captures an asymmetry between global types and configurations.
While Part~(a) shows that a configuration closely mimics the behavior of its associated global type, 
Part~(b) shows that a configuration may have more immediate behaviors than those described its associated global type:
this is because a configuration may include several 
independent (and immediate) reductions ($N_i$ above), which 
are matched by the global type only up to swapping.

\bigskip

\noi \textbf{Summing up,} we have that
Theorem~\ref{t:causal} ensures that reversibility in the atomic semantics is causally consistent.
 Theorem~\ref{t:bf} transfers this result to decoupled semantics; since by 
Theorem~\ref{t:corrgc} decoupled semantics defines a sound local implementation, we conclude that reversibility for global types is also causally consistent.

% !TEX root = revchor.tex

%\section{Extensions}\label{s:ext}
%TO DO.

\section{Related Work}\label{s:rw}
Reversibility in concurrency has received much attention recently. 
A detailed overview of the literature on the intersection between reversibility and 
behavioral contracts/types appears in~\cite[\S\,7]{MezzinaP17}. 
Within this research line, 
the works most related to ours are~\cite{DBLP:conf/rc/TiezziY16,DBLP:journals/corr/Dezani-Ciancaglini16a}.
%; such works, however,
%feature less expressive languages, 
%follow different approaches, and/or obtain results of different relevance. 
Tiezzi and Yoshida~\cite{DBLP:conf/rc/TiezziY16} study
the cost of implementing 
different ways of reversing binary and multiparty sessions; 
since they work in a \emph{synchronous} setting, 
these alternatives are simpler or incomparable to our asynchronous, decoupled rollback.
Dezani-Ciancaglini and Giannini~\cite{DBLP:journals/corr/Dezani-Ciancaglini16a} develop typed multiparty sessions with \emph{checkpoints},  points in the global protocol to which computation may return.   
While our reversible actions  are embedded in/guaranteed by the semantics, rollbacks in~\cite{DBLP:journals/corr/Dezani-Ciancaglini16a} should specify the name of the checkpoint to which computation should revert.
Defining reversibility in~\cite{DBLP:journals/corr/Dezani-Ciancaglini16a} requires modifying both processes and types. In contrast, we consider standard untyped processes and  local types (with cursors) as monitors. 
While we show causal consistency with a direct proof, in~\cite{DBLP:journals/corr/Dezani-Ciancaglini16a} causal consistency follows indirectly, as a consequence of typing. 
Reversibility in our model is fine-grained in that we allow reversible actions concerning exactly two of the protocol participants; in~\cite{DBLP:journals/corr/Dezani-Ciancaglini16a} when a checkpoint is taken, also parties not related with that choice are forced to return to a checkpoint. 

%More broadly, 
%Barbanera et al. have studied reversible/retractable contracts from different perspectives~\cite{DBLP:journals/corr/BarbaneraDd14,BDLL15,DBLP:conf/coordination/Barbanerad16}. 
%Although behavioral types and contracts are conceptually similar, there are technical differences that make in-depth comparisons hard to obtain.

\section{Concluding Remarks}\label{s:conc}
We presented a process framework of reversible, multiparty asynchronous communication, built upon session-based concurrency. 
As illustrated in \S\,\ref{s:examp},
the distinguishing features of 
our framework 
(decoupled rollbacks and abstraction passing, including delegation) endow it with substantial 
expressiveness, improving on prior works.

Our processes/configurations are untyped, but their (reversible) behavior is governed by monitors derived from local (session) types.
In our view, our monitored approach to reversibility  
is particularly appropriate for specifying and reasoning about systems with 
components whose behavior may not be statically analyzed (e.g., legacy components or services available as black-boxes). 
A monitored approach is general enough to support also the analysis of reversible systems that combine typed and
untyped components.


We proved that our reversible semantics is \emph{causally consistent}, which ensures that reversing a computation leads  to a  state that could have been reached by performing only forward steps.
The proof is challenging (and, in our view, also interesting), as we must resort to an alternative atomic semantics for rollbacks (Fig.~\ref{fig:atom}). 
We then connected reversibility at the level of process/configurations with reversibility at the level of global types, therefore linking the operational and declarative levels of abstraction typical of choreographic approaches to correctness for communication-centric software systems.

\paragraph{Extensions and Future Work}
\added{As already mentioned, our framework does not include name passing, which is known to be representable, in a fully abstract way, using 
name abstractions~\cite{KPY2016}. Primitive support for name passing is not difficult, but would entail notational burden. 
We do not foresee difficulties to strengthen 
Theorem~\ref{t:corrgc} to cover global types with higher-order values.
Such an extension would entail replacing $\ladeq{P}{T}{x}$ with a type system for multiparty, higher-order sessions, 
which could be obtained by adapting known type systems for binary, higher-order sessions~\cite{tlca07,KPY2016}.
These extensions (name passing, typability) would allow us to relate our framework with known
typed frameworks for monitored networks (without reversibility) based on multiparty sessions~\cite{DBLP:journals/tcs/BocchiCDHY17}.}

%In our model, reversible steps are always enabled; 
In future work, we plan to 
 extend our framework with so-called \emph{reversibility modes}~\cite{MezzinaP17},
which implement \emph{controlled reversibility} by specifying 
 how many times a particular protocol step can be reversed---zero, one, or infinite times.
 (Currently all actions can be reversed infinite times.) 
 In a related vein, we plan to explore variants of our model in which certain protocol branches are ``forgotten'' after they have been reversed; this modification is delicate, because it would weaken the notion of causal consistency.
%, and requires modifications to the definition of global and local types, and of projection.

%\jp{We should say that 
%(i)  having a type system limits the kind of systems to be addressed (not always we can statically analysze the behavior of processes) and (ii) 
%forgetting about branches of a choice unavoidably leads to weaker notions of causal consistency.}



revchor-TR.tex
\documentclass[10pt]{article} 

\usepackage{xspace}
\usepackage{amsmath,amsthm}
\usepackage{hyperref}
\usepackage{mathpartir}
\usepackage{amssymb}
\usepackage{stmaryrd}
\usepackage{enumerate}
\usepackage{mathtools}
\usepackage{times,xcolor,libertine}
\usepackage{geometry}

\newtheorem{innercustomtm}{Theorem}
\newenvironment{tm}[1]
  {\renewcommand\theinnercustomtm{#1}\innercustomtm}


\theoremstyle{definition}
\newtheorem{lemma}{Lemma}[section]
\newtheorem{definition}{Definition}[section]
\newtheorem{proposition}{Proposition}[section]
\newtheorem{remark}{Remark}[section]
\newtheorem{example}{Example}[section]
\newtheorem{corollary}{Corollary}[section]
\newtheorem{theorem}{Theorem}[section]
\newtheorem{property}{Property}[section]



\newcommand{\Nat}{{\mathbb N}}
\newcommand{\Real}{{\mathbb R}}
%\def\lastname{Mezzina and P\'{e}rez}

\begin{document}
         \title{Causally Consistent Reversible Choreographies\thanks{Revision of May 25, 2017. This work was partially supported by COST Actions IC1201 (Behavioral Types for Reliable Large-Scale Software Systems), IC1402 (Runtime Verification beyond Monitoring), and IC1405 (Reversible Computation - Extending Horizons of Computing). P\'{e}rez has been partially supported by CNRS PICS project 07313 (SuCCeSS); he is also affiliated to the NOVA Laboratory for Computer Science and Informatics (NOVA LINCS - PEst/UID/CEC/04516/2013), Universidade Nova de Lisboa, Portugal.}} 
          \author{Claudio Antares Mezzina \\ IMT School for Advanced Studies Lucca, Italy
          \and 
          Jorge A. P\'{e}rez
          \\ University of Groningen \& CWI, Amsterdam, The Netherlands} 
          \date{March 20, 2017}

\maketitle

\begin{abstract} 
%Reversible programming models are foundational models of fault-tolerant, distributed communication.
Under a reversible semantics, computation steps can be undone. % as a response to unanticipated events.
This paper addresses the integration of reversible semantics into 
process languages for communication-centric systems, equipped with \emph{behavioral types}. 
%This integration must reconcile the \emph{memories} that support
%reversible actions and  \emph{monitors}, the run-time entities that govern communication protocols. 
In prior work, we introduced a \emph{monitors-as-memories} approach to seamlessly integrate
 reversible semantics into a process model in which concurrency is governed by \emph{session types} (a class of behavioral types), 
  covering binary (two-party) protocols with syn\-chro\-nous communications.
 Although such a model offers a simple setting for showcasing our approach, 
 its expressiveness is rather limited.
Here we substantially extend our approach, and use it to define reversible semantics for 
a very expressive process model that accounts for 
multiparty ($n$-party)  protocols (\emph{choreographies}),
asynchronous communication,
 decoupled rollbacks,
 and process passing.
As main technical result, we prove that our multiparty, reversible semantics is \emph{causally-consistent}.
\end{abstract}

%\begin{keyword}
%Concurrency, process calculi, 
%reversible semantics, multiparty session types,
%causal consistency
%\end{keyword}
%\end{frontmatter}
\input{macros}
\input{revchor-body}

%\input{intro}
%\input{model}
%\input{results}
%\input{concl}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Bibliography.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\input{rev_ses}


\bibliographystyle{abbrv}
\bibliography{session,biblio}

\newpage
\appendix
\input{appendix} 

\end{document}

sematom.tex
% !TEX root = revchor.tex

Our main insight is that  causal consistency for asynchronous communication can be established by considering
a \textit{coarser} synchronous reduction relation.
We define \emph{atomic} versions of the forward and backward reduction relations, relying on the rules in Fig.~\ref{fig:atom}. 
The \emph{forward  atomic reduction}, denoted $\fwa$, is  
the smallest evaluation-closed relation that satisfies Rules \fwcolor{(\textsc{AC})}  and \fwcolor{(\textsc{AS})} (Fig.~\ref{fig:atom}), together with Rules 
\fwcolor{(\textsc{Init})}, \fwcolor{(\textsc{Beta})}, and \fwcolor{(\textsc{Spawn})} (Fig.~\ref{fig:fw}). 
Similarly, the \emph{backward atomic reduction}, denoted  $\bka$, is  the smallest evaluation-closed relation that satisfies Rules \bkcolor{(\textsc{RAC})}  and \bkcolor{(\textsc{RAS})} (Fig.~\ref{fig:atom}), together with Rules 
\bkcolor{(\textsc{RInit})}, \bkcolor{(\textsc{RBeta})}, and \bkcolor{(\textsc{RSpawn})} (Fig.~\ref{fig:bk}). 
We then define the atomic reduction relation $\reda$ as $\fwa \cup \bka$.

\begin{figure*}[t!]
{%\small
\begin{mathpar}
\inferrule[\fwcolor{(AC)}]{\p = \er_1 \,\vee\, \p \in \names{\er_1, h_i} 
\and
\q = \er_2 \,\vee\, \q \in \names{\er_2, h_i}
 }{
\begin{array}{c}
\np{\key{\loc_1}{\er_1}}{ \conf{\stack{C}}{\bout{\ep{s}{\p}}{V}{P}}} \Par 
\moni{s_\p}{\myctxr{\ctx{T}}{\past  \ltout{\q}{U}{S}}}{\mytilde x}{\store} \Par 
%\\
\np{\key{\loc_2}{\er_2}}{\conf{\stack{C}}{\binp{\ep{s}{\q}}{y}{Q}}} \Par 
 \moni{s_\q}{\myctxr{\ctx{S}}{\past  \ltinp{\p}{U}{T}}}{\mytilde x}{\store}  \Par \codah{s}{h_i}{h_o}{} \\
 \fwa 
 \\
\np{\key{\loc_1}{\er_1}}{\conf{\stack{C}}{P}} \Par 
\moni{s_\p}{\myctxr{\ctx{T}}{ \ltoutp{\q}{U}{S}}}{\mytilde x}{\store} \Par 
%\\
\np{\key{\loc_2}{\er_2}}{\conf{\stack{C}}{Q}} \Par 
 \moni{s_\q}{ \myctxr{\ctx{S}}{\ltinpp{\p}{U}{T}}}{\mytilde x, y}{\store\upd{y}{V}} \Par 
\codah{s}{h_i\cons  \valueq{\q}{\p}{V}}{h_o } 
\end{array}
 }
 \and
  \inferrule*[left=\fwcolor{(AS)}]{
  \p = \er_1 \,\vee\, \p \in \names{\er_1, h_i} 
\and
\q = \er_2 \,\vee\, \q \in \names{\er_2, h_i}
   }{
 \begin{array}{c}
\np{\key{\loc_1}{\er_1}}{ \conf{\stack C}{\bsel{\ep{s}{\p}}{\lbl_i. P_i}_{i\in I}}}  \Par 
\moni{s_\p}{\myctxr{\ctx{S}}{\past \ltsel{\q}{\lbl_j}{S_j}{j}{J}} }{\mytilde x}{\store} 
\\
\np{\key{\loc_2}{\er_2}}{ \conf { \stack C}{\bbra{\ep{s}{\q}}{\lbl_i:Q_i}_{i \in I} } } \Par 
\moni{s_\p}{\myctxr{\ctx{T}}
{\past \ltbra{\p}{\lbl_j}{T_j}{j}{J}} }{\mytilde x}{\store} 
\Par 
\codah{s}{h_i}{h_o}{} 
\\
\fwa 
\\
\np{\key{\loc_1}{\er_1}}{ \conf { \stack C , \bbra{\ep{s}{\p}}{\lbl_l:P_l}_{l \in I\setminus w}}{ P_w} } \Par 
\moni{s_\p}{\myctxr{\ctx{S}}{\ltbrap{\q}{\lbl_j:S_j\,,\, \lbl_w:\past S_w}{j}{J\setminus w}} }{\mytilde x}{\store}
\\
\np{\key{\loc_2}{\er_2}}{ \conf{\stack C , \bsel{\ep{s}{\q}}{\lbl_l.Q_l}_{l\in I\setminus w} }{Q_w}}\Par 
\moni{s_\q}{\myctxr{\ctx{T}}{ \ltselp{\p}{\lbl_j:T_j \, , \, \lbl_w:\past T_w}{j}{J\setminus w} }}{\mytilde x}{\store} 
\Par 
\codah{s}{h_i \cons  \valueq{\p}{\q}{\lbl_w} }{h_o }{} 
\end{array}
 }

\and
\inferrule[\bkcolor{(RAC)}]{
\p = \er_1 \,\vee\, \p \in \names{\er_1, h_i} 
\and
\q = \er_2 \,\vee\, \q \in \names{\er_2, h_i}
 }{
\begin{array}{c}
\np{\key{\loc_1}{\er_1}}{\conf{\stack{C}}{P}} \Par 
\moni{s_\p}{\myctxr{\ctx{T}}{ \ltoutp{\q}{U}{S}}}{\mytilde x}{\store} \Par 
%\\
\np{\key{\loc_2}{\er_2}}{\conf{\stack{C}}{Q}} \Par 
 \moni{s_\q}{ \myctxr{\ctx{S}}{\ltinpp{\p}{U}{T}}}{\mytilde x, y}{\store\upd{y}{V}} \Par 
\codah{s}{h_i\cons  \valueq{\q}{\p}{V}}{h_o } 
\\ \bka \\
\np{\key{\loc_1}{\er_1}}{ \conf{\stack{C}}{\bout{\ep{s}{\p}}{V}{P}}} \Par 
\moni{s_\p}{\myctxr{\ctx{T}}{\past  \ltout{\q}{U}{S}}}{\mytilde x}{\store} \Par 
\np{\key{\loc_2}{\er_2}}{\conf{\stack{C}}{\binp{\ep{s}{\p}}{y}{Q}}} \Par 
 \moni{s_\q}{\myctxr{\ctx{S}}{\past  \ltinp{\p}{U}{T}}}{\mytilde x}{\store}  \Par \codah{s}{h_i}{h_o}{} \\
\end{array}
 }
\and
 \inferrule*[left=\bkcolor{(RAS)}]{ \p = \er_1 \,\vee\, \p \in \names{\er_1, h_i} 
\and
\q = \er_2 \,\vee\, \q \in \names{\er_2, h_i}}{
 \begin{array}{c}
\np{\key{\loc_1}{\er_1}}{ \conf { \stack C , \bbra{\ep{s}{\p}}{\lbl_l:P_l}_{l \in I\setminus w}}{ P_w} } \Par 
\moni{s_\p}{\myctxr{\ctx{S}}{\ltbrap{\q}{\lbl_j:S_j\,,\, \lbl_w:\past S_w}{j}{J\setminus w}} }{\mytilde x}{\store}
\Par
\\
\np{\key{\loc_2}{\er_2}}{ \conf{\stack C , \bsel{\ep{s}{\q}}{\lbl_l.Q_l}_{l\in I\setminus w} }{Q_w}}\Par 
\moni{s_\q}{\myctxr{\ctx{T}}{ \ltselp{\p}{\lbl_j:T_j \, , \, \lbl_w:\past T_w}{j}{J\setminus w} }}{\mytilde x}{\store} 
\Par 
\codah{s}{h_i \cons  \valueq{\p}{\q}{\lbl_w} }{h_o }{}
\\
\bka
\\
\np{\key{\loc_1}{\er_1}}{ \conf{\stack C}{\bsel{\ep{s}{\p}}{\lbl_i. P_i}_{i\in I}}}  \Par 
\moni{s_\p}{\myctxr{\ctx{S}}{\past \ltsel{\q}{\lbl_j}{S_j}{j}{J}} }{\mytilde x}{\store} 
\Par
\\
\np{\key{\loc_2}{\er_2}}{ \conf { \stack C}{\bbra{\ep{s}{\q}}{\lbl_i:Q_i}_{i \in I} } } \Par 
\moni{s_\p}{\myctxr{\ctx{T}}
{\past \ltbra{\p}{\lbl_j}{T_j}{j}{J}} }{\mytilde x}{\store}  \Par 
\codah{s}{h_i}{h_o}{} 
\end{array}
 }
 \end{mathpar}
 }
 \vspace{-4mm}
 \caption{Atomic semantics for configurations: Forward and backward reduction ($\fwa$ and $\bka$).}
 \label{fig:atom}
\end{figure*}

We start by introducing \emph{reachable} configurations: % and configurations in \emph{normal form}.

\begin{definition}\label{d:ic}%[Initial and Reachable configuration]
A configuration $M$ is \emph{initial} if
$M\equiv \news{\tilde n} \prod_{i}\myloc{\loc_i}{P_i}$. A configuration is 
\emph{reachable}, if it is derived from an initial
configuration by using $\red$.  A configuration is  
\emph{atomically reachable}, if it is derived from an initial configuration by using $\reda$. 
\end{definition}

%\begin{definition}A configuration $M$ is said to be in \emph{normal form} if
%$$M\equiv  \prod_{i}\myloc{\loc_i}{P_i} \Par \news{s} \big(\prod_{j}\np{\loc_j}{\conf{\stack C_j}{P_j}} \Par \prod_z
%\moni{s_\p}{ T_z }{\mytilde x_z}{\store_z} \Par \codah{s}{h_1}{h_2} \big)$$
%\end{definition}

\noindent
To relate the decoupled semantics $\red$ (cf. \S\,\ref{ss:semconf}) with the atomic reduction $\reda$ (just defined), we introduce the concept of \textit{stable} configuration. Roughly speaking, in a stable configuration there are no 
``ongoing'' reduction steps. In the forward case, 
an ongoing step is witnessed by non-empty output queues (which should eventually become empty to complete a synchronization);
in the backward case, an ongoing step is witnessed by a marked monitor
(which should be eventually unmarked when a synchronization is undone).
\added{This way, e.g., in the example of \S\,\ref{s:examp} configurations $M_3$ and $M_7$ are stable, whereas $M_2$ and $M_4$ are not stable.}
Reduction $\reda$ will move between stable configurations only.
We therefore have:
\begin{definition}%[Stable configuration]
\label{lm:fwstable}
A configuration $M$ is  \emph{stable}, written $\stable(M)$, if 
\begin{align*}
M & \equiv  \prod_{i}\myloc{\loc_i}{P_i} \Par 
\news{s\tilde{a}} \big(\prod_{j}\np{\key{\loc_j}{\p_j}}{\conf{\stack C_j}{P_j}} \Par 
\\
&
\qquad \qquad \qquad \qquad
%\\
%\qquad
%\prod_z \hmoni{s_{\p_z}}{ T_z }{\mytilde x_z}{\store_z} 
\hmoni{s_{\p_i}}{ T_i }{\mytilde x_i}{\store_i} 
\Par \codah{s}{h_1}{\emp} \big)
\end{align*}

\end{definition}


\noindent
Reduction $\red$ does not preserve stability, but it can be recovered: % with one or two steps:

\begin{lemma}
Given $M$ a stable configuration then
\begin{enumerate}[$\bullet$]
	\item if $M\fw N$ with $\lnot\stable(N)$ then there exists an $N'$ such that $N\fw N'$ and $\stable(N')$; 
	\item if $M\bk N$ with $\lnot\stable(N)$ then there exists an $N'$ such that $N\bk\bk N'$ and $\stable(N')$.
\end{enumerate}
\end{lemma}

%\begin{proof}
%Follows directly from the definition of $\fw$ and $\bk$.
%\end{proof}

We may then have:

\begin{corollary}\label{lbl:corollary_finish}
If $\stable(M)$ and $M\trans\red N$ with $\lnot\stable(N)$, then there exists an $N'$ such that $N\trans\red N'$ with $\stable(N')$.
\end{corollary}
\begin{proof}
By induction on the reduction sequence $M \trans{\red}N$.
\end{proof}

\noindent
We now show the Loop lemma~\cite{DBLP:conf/concur/DanosK05}, which ensures that every reduction step can be reverted. 
This lemma will be crucial both in proving a correspondence between atomic and decoupled semantics, and in showing causal consistency of the atomic semantics.

\begin{lemma}[Loop]\label{lemma:loop}
Let  $M, N$ be stable and atomic reachable configurations. Then 
%$M\fwa N \iff N\bka M$.
$M\fwa N$ if and only if $N\bka M$.

\end{lemma}
\begin{proof}
By induction on the derivation of $M\fwa   N$ for the if direction, and on the derivation of $N \bka  M$ for the converse.
\end{proof}

\noindent The following lemma allow us to ``rearrange''  atomic reduction steps; 
it will be useful to connect atomic and decoupled reductions.

\begin{lemma}[Swap]\label{lemma:swap}
Let $M$ be a reachable configuration, then:
\begin{enumerate}[$\bullet$]
\item If $M\fws N_1$ using Rules~\fwcolor{(\textsc{Out})} or ~\fwcolor{(\textsc{Sel})}, and $N_1 \fw N_2$ by using Rules~\fwcolor{(\textsc{In})} or ~\fwcolor{(\textsc{Sel})} then $M\fw\fw N{\fws} N_2$, for some $N$;
\item If $M\bks N_1$ using Rules~\bkcolor{(\textsc{ROut})} or ~\bkcolor{(\textsc{RSel})}, and $N_1 \bk N_2$ by using Rules~\bkcolor{(\textsc{RIn})} or ~\bkcolor{(\textsc{RSel})} then $M\bk\bk N\bks N_2$, for some $N$. 
\end{enumerate}
\end{lemma}
%\begin{proof}
%Both cases are similar. We proceed by induction on the number of reductions in $M\trans{\fw} N_1$ ($M\trans{\bk} N$) and by case analysis on the last applied rule.
%\end{proof}

%The intention is that the coarser semantics will move between stable configurations:
%\begin{lemma}\label{lemma:corr}
%Let $M$ and $N$ be stable configurations: 
%	\begin{itemize}
%		\item If $M \fwa N $ then either $M \fw N$ or $M \fw \fw N$ 
%		\item If $M \bka N $ then  either $M\bk N$ or $M \bk \bk \bk N$
%	\end{itemize} 
%\end{lemma}

\noindent
The following theorem is a first   connection between decoupled and atomic reductions; its proof is immediate from their definitions:
\begin{theorem}[Relating $\red$ and $\reda$]\label{theo:correspond}
Let $M$ and $N$ be stable configurations. We have:
\begin{enumerate}[$\bullet$]
	\item $M\fwa N$ if and only if either $M{\fw} N$ or $M{\fw\fw} N$;
	\item $M\bka N$ if and only if either  $M{\bk} N$ or $M{\bk\bk\bk} N$.
\end{enumerate}
\end{theorem}
%\begin{proof}
%\end{proof}
\noindent
We now embark ourselves in providing a tighter formal connection between $\red$ and $\reda$, using \emph{back-and-forth bisimulations}~\cite{LaneseMS16}.
We shall work with binary relations on configurations, written $\Re  \subseteq \confs \times \confs$.
We now adapt the classical notion of barbs~\cite{DBLP:conf/concur/SangiorgiW01} to our setting:
rather than communication subjects (which are hidden/unobservable names in intra-session communications), 
it suffices to use participant identities as observables:
\begin{definition}[Barbs]\label{lbl:barb}
A reachable configuration $M$ has a barb $\p$, written $M\barb{\p}$, 
if
\begin{enumerate}[$\bullet$]
\item $M\equiv \news{\vect n} (N \Par \np{\key{\loc}{\er}}{\conf{\stack C}{P}} \Par \moni{s_\p}{ \ctx{S}[\past T] }{\mytilde x}{\store})$ where either: \\  
(i)~$P\equiv \bout{\ep{s}{\p}}{V}{Q} \Par R$ and $T=\ltout{\q}{U}{T_1} $ or  \\
(ii)~$P\equiv \bsel{\ep{s}{\p}}{\lbl_i.P_i}_{i\in I}\Par R$ and $T= \ltsel{\q}{\lbl_j}{T_j}{j}{J}$. 
\end{enumerate}
\end{definition}
\noindent
Notice that our definition of barbs is connected to the notion of stability:
since in 
$M\barb{\p}$ 
we require a monitor with empty tag, this ensures that 
$\p$ is not involved in an ongoing backward step. 
In a way, this allows us to consider just \textit{forward barbs} (as in~\cite{DBLP:journals/jlp/AubertC17}). 

We now  adapt the definition of weak barbed back-and-forth (bf) bisimulation and congruence~\cite{LaneseMS16} in order to work with 
decoupled and atomic reduction semantics:
%\begin{definition}
%A relation $\Re \subseteq \confs \times \confs$ is a strong (resp. weak) barbed bf simulation if whenever $M \Re N$
%\begin{itemize}
%	\item $M\barb{\p}$ implies $N\barb{\p}$ (resp. $M\trans{\red}\barb{\p}$) 
%	\item $M\fwa M_1$ implies $N\fw N_1$, with $M_1 \Re N_1$ 
%	(resp. $N\trans{\fw} N_1$, with $M_1 \Re N_1$);
%	\item $M\bka M_1$ implies $N\bk N_1$, with $M_1 \Re N_1$ 
%	(resp. $N\trans{\bk} N_1$, with $M_1 \Re N_1$);
%\end{itemize}
%A relation $\Re \subseteq \confs \times \confs$ is a strong (resp. weak) barbed bisimulation \text{if}
% $\Re$  and  $\Re^{-1}$ are strong (resp. weak) barbed simulations.
% We call strong
%(resp. weak) barbed bisimilarity and note $\bfb$ (resp. $\bfbw$) the largest strong (resp. weak) barbed bisimulation. We say that two configurations $M$ and $N$ are strong (resp. weak) barbed congruent, written 
% $\congruence{\bfb}$ (resp. $\congruence{\bfbw}$), 
% if for each context $ \ctx{C}$ such that $\ctx{C}[M]$ and 
% $\ctx{C}[N]$ are reachable configurations, then $C[M] \bfb C[N]$ (resp. $C[M] \bfbw C[N]$).
\begin{definition}\label{d:bf}
A relation $\Re$ is a \emph{(weak) barbed bf simulation} if whenever $M \Re N$
\begin{enumerate}
	\item $M\barb{\p}$ implies $N\trans{\red}\barb{\p}$; 
	\item $M\fwa M_1$ implies $N\trans\fw N_1$, with $M_1 \Re N_1$; 
	\item $M\bka M_1$ implies $N\trans\bk N_1$, with $M_1 \Re N_1$.
\end{enumerate}
A relation $\Re$ is a  \emph{(weak) barbed bisimulation} if
 $\Re$  and  $\Re^{-1}$ are  weak bf barbed simulations.
 The largest weak barbed bisimulation is  
\emph{(weak) barbed bisimilarity},  noted $\bfbw$. 
$M$ and $N$ are \emph{(weakly) barbed congruent}, written 
$\congruence{\bfbw}$, 
 if for each context $\ctx{C}$ such that $\ctx{C}[M]$ and  $\ctx{C}[N]$ are 
atomic reachable configurations, then
 $\ctx{C}[M] \bfbw \ctx{C}[N]$.
\end{definition}

\noindent We now may state our second connection between decoupled and atomic reductions:

\begin{theorem}\label{t:bf}
For any atomic reachable configuration $M$, we have that $M \congruence\bfbw M$.
\end{theorem}
\begin{proof}[Proof (Sketch)]
It suffices to show that the following relation is a 
bf weak bisimulation:
\begin{align*}
	\Re =\{ (M,N) \st  M \trans{\fw} N \text{ via Rules~\fwcolor{(\textsc{Out})} or \fwcolor{(\textsc{Sel})}} ~ \wedge   
	\\
M \trans{\bk} N \text{ via Rules~\bkcolor{(\textsc{ROut})} or \bkcolor{(\textsc{RSel}})} \} 
\end{align*}
The analysis uses Corollary~\ref{lbl:corollary_finish}, Theorem~\ref{theo:correspond}, 
 the Loop and Swap Lemmas (Lemmas~\ref{lemma:loop} and~\ref{lemma:swap}).
See App.~\ref{app:bf} for details.
\end{proof}

\noindent
By observing that the set of 
atomic configurations is a subset of reachable configurations, 
this result can also be  formulated as full abstraction. 
Let $f$ be the (injective, identity) mapping 
from atomic reachable configurations to reachable configurations. We then have:

\begin{corollary}[Full Abstraction]
Let $f$ be the injection from atomic reachable configurations to reachable configurations, and let $M, N$ 
be two atomic reachable configurations. 
Then we have $f(M) \congruence\bfbw f(N)$ if and only if $M \congruence\bfbw N$.
\end{corollary}
\begin{proof}
From Theorem~\ref{t:bf} we have $M\congruence\bfbw f(M)$ and 
$N\congruence\bfbw f(N)$. The thesis follows then by transitivity of $\congruence\bfbw$.
\end{proof}
The results above ensure that the loss of atomicity  preserves the reachability of configurations yet does not make undesired configurations reachable.

%\begin{proof}
%First, notice that showing $\ctx{C}[M]\bfbw\ctx{C}[M]$ is similar to show 
%$M_1 \bfbw M_1$ with $M_1 = \ctx{C}[M]$.
%This allows us to just focus on the ``hole'' of the context. 
%It is then sufficient to show that the following relation is a 
%bf weak bisimulation. 
%\begin{align*}
%	\Re =\{ (M,N) \st  M \trans{\fw} N \text{ via Rules~\textsc{Out} or \textsc{Sel}} \wedge   
%M \trans{\bk} N \text{ via Rules~\textsc{ROut} or \textsc{RSel}} \} 
%\end{align*}
%Clearly, $(M, M) \in \Re$. We consider the requirements in Def.~\ref{d:bf}.
%
%Let us first consider barbs. Suppose that $M$ challenges $N$ with a barb, 
%we distinguish two cases: $N$ is stable or not.
%If
% $\stable(N)$  then $N$  has the same barb. Otherwise,  if $\lnot\stable(N)$,
% by  Corollary~\ref{lbl:corollary_finish} 
% there exists an $N_1$ such that
% $N\trans{\red} N_1$ and $\stable(N_1)$.
% Since $M \trans{\red} N$ 
%  we may derive $M\trans{\red} N_1$ with both stable configurations. 
%  By applying Theorem~\ref{theo:correspond} on $M\trans{\red} N_1$ we infer $M\trans{\reda} N_1$;
%  then, by
% applying the Loop Lemma (Lemma~\ref{lemma:loop})  we further infer $N_1\trans{\reda} M$. 
% Using again Theorem~\ref{theo:correspond} we infer that $N_1\trans{\red} M$; 
% since we have deduced that $N\trans{\red} N'\trans{\red} M$,
% we know that $N$ weakly matches all the barbs of $M$, as desired. 
% Suppose now that $N$ challenges $M$ with a barb.
% We proceed similarly as above:
%  if $\stable(M)$ then $M$ has the same barb; otherwise, if $\lnot\stable(M)$, since $M\trans{\red} N$, by Corollary~\ref{lbl:corollary_finish} we have that $M\trans{\red} N \trans{\red}N_1$, with $\stable(N_1)$.
% Let us note that the reductions in $N\trans{\red} N_1$ do not add barbs to $N_1$: they only finalize ongoing synchrinizations; by definition of barbs (Def.~\ref{lbl:barb}) parties involved in ongoing rollbacks do not contribute to barbs. We can conclude by applying Theorem~\ref{theo:correspond} and deriving $M\trans{\reda} N_1$, which has the same barbs of $N$, as desired. 
% 
% % and has the same barbs of $N_1$ since messages and branches involved in ongoing backward steps are not considered barbs (Definition~\ref{lbl:barb}).
% 
% Let us now consider reductions. We will just focus on synchronizations due to input/output and branching/selection reduction steps, since 
% these are the cases in which $\red$ and $\reda$ differ; indeed, 
% the cases of \textsc{Spawn} and \textsc{Beta} are trivially matched. There are two cases: $M\fwa M_1$ and $M\bka M_1$.
% In the first case, as  we distinguish two sub-cases: either $N$ has already started the synchronization or not. In the first case, $N$ can conclude the step: $N\fw N'$. Now we have that
% $M\trans{\fw} N\fw N'$. Thanks to Lemma~\ref{lemma:swap} we can rearrange such reduction sequence as follows: $M\fw\fw M_1\trans{\fw} N'$. We then have that the pair $(M_1,N')\in \Re$, as desired. In the second case,
% $N$ can match the step with 2 reductions: $N\fw \fw N'$. Also in this case we can rearrange the reduction 
% sequence so as to obtain $M\fw\fw M_1\trans{\fw} N'$, with  $(M_1,N')\in \Re$, as desired. 
%The second case is when $M\bka M_1$ (i.e., the challenge is a backward move) and is handled similarly. 
% 
%We now consider challenges from $N$, focusing only on synchronizations, just as before.
% %we will just focus on communications steps, since the case of \textsc{Spawn} and \textsc{Beta} is trivially matched.  
% If $N\fw N'$, we distinguish two cases: whether the reduction finalizes ends an ongoing  input/output and branching/selection, or it opens a new one. 
%   In the second case $M$ matches the move with an idle move, i.e.,
% $(M,N')\in \Re$. In the other case   we can rearrange the reduction $M\trans{\fw}N\fw N'$ to a similar reduction 
% $M\trans{\red} N_1\trans{\fw} N'$ with $\stable(N_1)$, and all reductions  in $N_1\trans\fw N'$ just start new synchronizations. 
% Thanks to Theorem~\ref{theo:correspond}, $M$ can mimick the same reduction to $N_1$, i.e., $M\trans\fwa N_1$, and we have that $(N_1,N')\in \Re$, as desired. 
% The case in which $N \bk N'$ (i.e., the challenge is a backward move) is similar. This concludes the proof.
%\end{proof}

semdec.tex
% !TEX root = revchor.tex




%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{figure*}[t!]
{%\small
\begin{mathpar}
\inferrule*[left=\fwcolor{(Init)}]
{\parties{G}= \{\p_1,\cdots,\p_n\} \and 
\forall \gpart{p}_i\in \parties{G}. \, \tproj{G}{\gpart{p}_i} = T_{i}  } 
{ 
\begin{array}{c}
\myloc{\loc_1}{\bout{a}{x_1:T_1}{P_{1}}} \Par 
\prod_{i \in \{2, \cdots, n\}}\myloc{\loc_i}{\binp{a}{x_i:T_i}{P_{i}}} 
\\
~\fw~ 
\\
\news{s} \Big(\, 
\prod_{i \in\{1,\cdots,n\}} \np{\key{\loc_i}{\p_i}}{ \conf{\inact}{P_i\subst{\ep{s}{\p_i}}{x_i}}} \Par 
\moni{s_{\p_i}}{\past T_{i}}{x_i}{\upd{x_i}{a }}  \Par \codah{s}{\emp}{\emp}{}\Big)
\end{array}
}
\and
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\inferrule*[left = \fwcolor{(Out)}]{ \p = \er \,\vee\, \p \in \names{\er, h_i} }{
\begin{array}{c}
\np{\key{\loc}{\er}}{ \conf{\stack{C}}{\bout{\ep{s}{\p}}{V}{P}}} \Par \moni{s_\p}{\myctxr{\ctx{T}}{\past  \ltout{\q}{U}{S}}}{\mytilde x}{\store} \Par \codah{s}{h_i}{h_o}{}  
\\
\fw 
\\
\np{\key{\loc}{\er}}{\conf{\stack{C}}{P}} \Par \moni{s_\p}{\myctxr{\ctx{T}}{ \ltoutp{\q}{U}{S}}}{\mytilde x}{\store} \Par 
\codah{s}{h_i}{h_o\cons \valueq{\p}{\q}{\myeval{V}{\sigma}}}{}
\end{array}
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\and 
%
\inferrule*[left = \fwcolor{(In)}]{
\p = \er \,\vee\, \p \in \names{\er, h_i}
}
{\begin{array}{c}
\np{\key{\loc}{\er}}{\conf{\stack{C}}{\binp{\ep{s}{\p}}{y}{P}}} \Par \moni{s_\p}{\myctxr{\ctx{T}}{\past  \ltinp{\q}{U}{S}}}{\mytilde x}{\store} \Par \codah{s}{h_i}{\valueq{\q}{\p}{V}\cons h_o }{}
\\
\fw 
\\
\np{\key{\loc}{\er}}{\conf{\stack{C}}{P}} \Par \moni{s_\p}{ \myctxr{\ctx{T}}{\ltinpp{\q}{U}{S}}}{\mytilde x, y}{\store\upd{y}{V}} \Par 
\codah{s}{h_i\cons  \valueq{\q}{\p}{V}}{h_o }{} 
\end{array}
} 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\and
\inferrule[\fwcolor{(Sel)}]
{\p = \er \,\vee\, \p \in \names{\er, h_i}
\and
w\in J \and J\subseteq I }
{ 
\begin{array}{c}
\np{\key{\loc}{\er}}{ \conf{\stack C}{\bsel{\ep{s}{\p}}{\lbl_i. P_i}_{i\in I}}}  \Par 
\moni{s_\p}{\myctxr{\ctx{T}}{\past \ltsel{\q}{\lbl_j}{S_j}{j}{J}} }{\mytilde x}{\store} \Par \codah{s}{h_i}{h_o}{} \quad 
\\
\fw 
\\
\np{\key{\loc}{\er}}{ \conf{\stack C , \bsel{\ep{s}{\p}}{\lbl_i.P_i}_{i\in I\setminus w} }{P_w} }\Par 
\moni{s_\p}{ \myctxr{\ctx{T}}{ \ltselp{\q}{\lbl_j:S_j \, , \, \lbl_w:\past S_w}{j}{J\setminus w}} }{\mytilde x}{\store} 
%\\
%\quad \qquad
\Par 
\codah{s}{h_i}{h_o\cons  \valueq{\p}{\q}{\lbl_w} }{} 
\end{array} 
 }
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\and
\inferrule[\fwcolor{(Bra)}]{\p = \er \,\vee\, \p \in \names{\er, h_i} 
\and w\in I \and I\subseteq J }
{
\begin{array}{c}
\np{\key{\loc}{\er}}{ \conf { \stack C}{\bbra{\ep{s}{\p}}{\lbl_i:P_i}_{i \in I} } } \Par \moni{s_\p}{\myctxr{\ctx{T}}
{\past \ltbra{\q}{\lbl_j}{S_j}{j}{J}} }{\mytilde x}{\store} \Par \codah{s}{h_i}{\valueq{\q}{\p}{\lbl_w}\cons h_o}{} 
\\
\fw 
\\
\np{\key{\loc}{\er}}{ \conf { \stack C , \bbra{\ep{s}{\p}}{\lbl_i:P_i}_{i \in I\setminus w}}{ P_w} } \Par 
\moni{s_\p}{\myctxr{\ctx{T}}{\ltbrap{\q}{\lbl_j:S_j\,,\, \lbl_w:\past S_w}{j}{J\setminus w}} }{\mytilde x}{\store}
%\\
%\quad  \qquad 
\Par \codah{s}{h_i\cons  \valueq{\q}{\p}{\lbl_w}}{h_o}{}
\end{array}
 }
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\and
%
\inferrule[\fwcolor{(Beta)}]{\myeval{V}{\sigma} =\abs{x}{P} }
{
\begin{array}{l}
\np{\key{\loc}{\p}}{\conf{\stack{C}}{(\appl{V}{w})}} \Par \moni{s_\p}{\myctxr{\ctx{T}}{\past S}}{\mytilde x}{\store} 
~\fw~ 
\news{k}\, \left( {\np{\key{\loc}{\p}}{\conf{\ctx{\stack {C}}}{P\subst{\myeval{w}{\sigma}}{x}}}}  \Par \mem{k}{(\appl{V}{w})}{\loc} \Par\moni{s_\p}{\myctxr{\ctx T}{ k. \past S}}{\mytilde x}{\store} \right)
\end{array}
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\and
%
\inferrule[\fwcolor{(Spawn)}]{ }
{
\begin{array}{c}
\np{\key{\loc}{\p}}{\conf{\stack{C}}{P \Par Q}} \Par \moni{s_\p}{\myctxr{\ctx{T}}{\past S}}{\mytilde x}{\store} 
\\
~\fw~ 
\\
\news{\loc_1,\loc_2}\, \left( \np{\key{\loc}{\p}}{\conf{\stack{C}}{\inact}}  
\Par \np{\key{\loc_1}{\p}}{\conf{\inact}{P}}
\Par \np{\key{\loc_2}{\p}}{\conf{\inact}{Q}} 
\Par \moni{s_\p}{\myctxr{\ctx T}{ (\loc,\loc_1,\loc_2). \past S}}{\mytilde x}{\store} \right)
\end{array}
}

\end{mathpar}
}
\vspace{-5mm}
\caption{Decoupled semantics for configurations: Forward reduction ($\fw$).}
\label{fig:fw}
\end{figure*}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{figure*}[t!]
{%\small
\begin{mathpar}
\inferrule*[left=\bkcolor{(RInit)}]
{\parties{G}= \{\p_1,\cdots,\p_n\} \and 
\forall \gpart{p}_i\in \parties{G}. \, \tproj{G}{\gpart{p}_i} = T_{i} \and P_i = Q_{i}\subst{\ep{s}{\p_i}}{x} } 
{ 
\begin{array}{c}
\news{s} \left(\, 
\prod_{i \in\{1,\cdots,n\}} \np{\key{\loc_i}{\p_i}}{ \conf{\inact}{Q_i}} \Par 
\hmoni{s_{\p_i}}{\past T_{i}}{x_i}{\upd{x_i}{a }}  \Par \codah{s}{\emp}{\emp}{}\right)
\\
~\bk~
\\
\myloc{\loc_1}{\bout{a}{x_1:T_1}{P_{1}}} \Par 
\prod_{i \in \{2, \cdots, n\}} \myloc{\loc_i}{\binp{a}{x_i:T_i}{P_i}}
\end{array}
}
\and
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\inferrule*[left=\bkcolor{(RollS)}]{ }{
\begin{array}{c}
\hmoni{s_\p}{ \myctxr{\ctx T}{\ltinpp{\q}{U}{T}}}{\mytilde x}{\store_1} \Par 
\hmoni{s_\q}{ \myctxr{\ctx S}{\ltoutp{\p}{U}{S}}}{\mytilde y}{\store_2} \Par 
%\codah{s}{h_i}{h_o}{\restrict{\mytilde{\gpart{r}}}}
\codah{s}{h_i}{h_o}
%\quad 
\\
\bk 
\\
\monir{s_\p}{ \myctxr{\ctx T}{\ltinpp{\q}{U}{T}}}{\mytilde x}{\store_1} \Par 
\monir{s_\q}{\myctxr{\ctx S}{\ltoutp{\p}{U}{S}}}{\mytilde y}{\store_2} \Par 
%\codah{s}{h_i}{h_o}{\restrict{\mytilde{\gpart{r}},\p,\q}}
\codah{s}{h_i}{h_o}
\end{array}
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\and 
%
\inferrule[\bkcolor{(RollC)}]{ }{
\begin{array}{c}
\hmoni{s_\p}{\myctxr{\ctx T}{\ltbrap{\q}{\lbl_z:\past S_z\,,\,\lbl_w:S_w}{z}{J\setminus w}}}{\mytilde x}{\store_1}  \Par 
\hmoni{s_\q}{\myctxr{\ctx S}{\ltselp{\p}{\lbl_z:\past S_z \, , \, \lbl_w: S_w}{z}{J\setminus w}}}{\mytilde y}{\store_2}  \Par 
%\codah{s}{h_i}{h_o}{\restrict{\mytilde{\gpart{r}}}}
\codah{s}{h_i}{h_o}
\\
\bk 
\\
\monir{s_\p}{ \myctxr{\ctx T}{\ltbrap{\q}{\lbl_z:\past S_z\,,\,\lbl_w:S_w}{z}{J\setminus w}}}{\mytilde x}{\store_1}  \Par 
\monir{s_\q}{\myctxr{\ctx S}{\ltselp{\p}{\lbl_z:\past S_z \, , \, \lbl_w: S_w}{z}{J\setminus w}}}{\mytilde y}{\store_2}  \Par 
%\codah{s}{h_1}{h_2}{\restrict{\mytilde{\gpart{r}},\p,\q}}
\codah{s}{h_i}{h_o}
\end{array}
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\and
%
\inferrule*[left=\bkcolor{(ROut)}]{ \p = \er \,\vee\, \p \in \names{\er, h_i}}
{
\begin{array}{l}
\np{\key{\loc}{\er}}{\conf{\stack C}{P}} \Par \monir{s_\p}{ \myctxr{\ctx T}{\ltoutp{\q}{U}{S}} }{\mytilde x}{\store}
\Par 
%\codah{s}{h_i}{(\p,\q,V)\cons h_o}{\restrict{\p,\mytilde{\gpart{r}}}}
\codah{s}{h_i}{(\p,\q,V)\cons h_o}
\\
~\bk~
\\
\np{\key{\loc}{\er}}{\conf{\stack C }{\bout{\ep{s}{\p}}{V}{P}}} \Par 
\hmoni{s_\p}{ \myctxr{\ctx T}{\past\ltout{\q}{U}{S}} }{\mytilde x}{\store}
 \Par %\codah{s}{h_i}{h_o}{\restrict{\mytilde{\gpart{r}}}}
 \codah{s}{h_i}{h_o}
\end{array}
 }
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\and
%
\inferrule*[left=\bkcolor{(RIn)}]{ 
\p = \er \,\vee\, \p \in \names{\er, h_i}
}
{
\begin{array}{c}
\np{\key{\loc}{\er}}{\conf{\stack C}{P}} \Par 
\monir{s_\p}{ \myctxr{\ctx T} {\ltinpp{\q}{U}{S}} }{\mytilde x,y}{\store} \Par 
%\codah{s}{h_i\cons(\q,\p,V)}{h_o}{\restrict{\p,\mytilde{\gpart{r}}}}
\codah{s}{h_i\cons(\q,\p,V)}{h_o}
\\
\quad \bk
\\
\np{\key{\loc}{\er}}{\conf{\stack C} { \binp{\ep{s}{\p}}{y}{P}} } \Par 
\hmoni{s_\p}{ \myctxr{\ctx T}{\past\ltinp{\q}{U}{S}}}{\mytilde x}{\rup{\store}{y}}\Par %\codah{s}{h_i}{(\q,\p,V)\cons h_o}{\restrict{\mytilde{\gpart{r}}}}
\codah{s}{h_i}{(\q,\p,V)\cons h_o}
\end{array}
 }
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\and
\inferrule[\bkcolor{(RBra)}]
{ \p = \er \,\vee\, \p \in \names{\er, h_i} \and w \in I \and I\subseteq J} 
{
\begin{array}{c}
\np{\key{\loc}{\er}}{\conf{\stack C,\bbra{\ep{s}{\p}}{\lbl_i:P_i }_{i \in I\setminus\set{w}}}{P}
} \Par 
\monir{s_\p}{\myctxr{\ctx T}{\ltbrap{\q}{\lbl_j:S_j\,,\, \lbl_w:\past S_w}{j}{J\setminus w}} }{\mytilde x}{\store}
\Par 
%\codah{s}{h_i\cons  \valueq{\q}{\p}{\lbl_w}}{h_o}{\restrict{\p, \mytilde{\gpart{r}}}}
\codah{s}{h_i\cons  \valueq{\q}{\p}{\lbl_w}}{h_o}
\\
\quad \bk 
\\%[1mm]
\np{\key{\loc}{\er}}{ \conf{\stack C}{\bbra{\ep{s}{\p}}{\lbl_i:P_i, \lbl_w : P }_{i \in I\setminus\set{w}}}} \Par 
\hmoni{s_\p}{\myctxr{\ctx T}{\past\ltbra{\q}{\lbl_j}{S_j}{j}{J}} }{\mytilde x}{\store} 
\Par 
%\codah{s}{h_i}{\valueq{\q}{\p}{\lbl_w}\cons h_o}{\restrict{\mytilde{\gpart{r}}}}
\codah{s}{h_i}{\valueq{\q}{\p}{\lbl_w}\cons h_o}
\end{array}
 }
\and 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\inferrule*[left=\bkcolor{(RSel)}]
{ \p = \er \,\vee\, \p \in \names{\er, h_i} \and w \in I \and I\subseteq J} 
{
\begin{array}{c}
\np{{\key{\loc}{\er}}}{ \conf{\stack C,\bsel{\ep{s}{\p}}{\lbl_i. P_i}_{i\in I} }{P}} \Par 
\monir{s_\p}{ \myctxr{\ctx T}{ \ltselp{\q}{\lbl_j:S_j \, , \, \lbl_w:\past S_w}{j}{J\setminus w} } }{\mytilde x}{\store}
\Par 
%\codah{s}{h_i}{\valueq{\p}{\q}{\lbl_w}\cons h_o}{\restrict{\p,\mytilde{\gpart{r}}}}
\codah{s}{h_i}{\valueq{\p}{\q}{\lbl_w}\cons h_o}
\\
\quad \bk 
\\
\np{{\key{\loc}{\er}}}{ \conf{\stack C}{ \bsel{\ep{s}{\p}}{\lbl_w. P} + \bsel{\ep{s}{\p}}{\lbl_i. P_i}_{i\in I} } } \Par 
\hmoni{s_\p}{ \myctxr{\ctx T}{ \past \ltsel{\q}{\lbl_j}{S_j}{j}{J} } }{\mytilde x}{\store} \Par 
%\codah{s}{h_i}{h_o}{\restrict{\mytilde{\gpart{r}}}}
\codah{s}{h_i}{h_o}
\end{array}
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\and
%
\inferrule*[left=\bkcolor{(RBeta)}]{ }
{
\begin{array}{l}
\news{k}\,\left( {\np{\key{\loc}{\p}}{\conf{\stack{C}}{Q} }}  \Par \mem{k}{(\appl{V}{w})}{\loc} \Par\moni{s_\p}{\myctxr{\ctx T}{ k. \past S}}{\mytilde x}{\store}
\right)
%\\
~\bk~ 
%\\
\np{\key{\loc}{\p}}{\conf{\stack{C}}{(\appl{V}{w})}} \Par \moni{s_\p}{\myctxr{\ctx{T}}{\past S}}{\mytilde x}{\store} 
\end{array} 
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \and
\inferrule[\bkcolor{(RSpawn)}]{ }
{
\begin{array}{c}
\news{\loc_1,\loc_2}\, \left( {\np{\key{\loc}{\p}}{\conf{\stack{C}}{\inact}}}  
\Par \np{\key{\loc_1}{\p}}{\conf{\inact}{P}}
\Par \np{\key{\loc_2}{\p}}{\conf{\inact}{Q}} 
\Par \moni{s_\p}{\myctxr{\ctx T}{ (\loc,\loc_1,\loc_2). \past S}}{\mytilde x}{\store} \right)
\\
~\bk~
\\
\np{\key{\loc}{\p}}{\conf{\stack{C}}{P \Par Q}} \Par \moni{s_\p}{\myctxr{\ctx{T}}{\past S}}{\mytilde x}{\store}  
\end{array}
}

\end{mathpar}
}
\vspace{-4mm}
\caption{Decoupled semantics for configurations: Backwards reduction ($\bk$).}
\label{fig:bk}
\vspace{-3mm}
\end{figure*}

semglobal.tex
% !TEX root = revchor.tex

\begin{figure}[t!]
{%\small
\begin{mathpar}
%\inferrule[(Act)]{\ctx{G'} [\bullet]= \ctx{G}[\gpart{p}\to\gpart{q}:\{l_i\langle U_i\rangle.G_i \,;\, l_i\langle U_j\rangle.\bullet\}_{i \in I\setminus j} ]}
%{\ctx{G}[ \past \gtact{p}{q}{l_i}{U_i}{G_i}] \fw \ctx{G'}[\past G_j]}
%\\
%\inferrule[(Act1)]{ }
%{\ctx{G}[ \past \gtact{p}{q}{l_i}{U_i}{G_i}] 
%\fw 
%\ctx{G}[\gpart{p}\to\!\past\gpart{q}:\{l_i\langle U_i\rangle.G_i \,;\, l_j\langle U_j\rangle.G_j\}_{i \in I\setminus j} ]}
%\\
%\inferrule[(Act2)]{ }
%{\ctx{G}[\gpart{p}\to\!\past\gpart{q}:\{l_i\langle U_i\rangle.G_i \,;\, l_j\langle U_j\rangle.G_j\}_{i \in I\setminus j} ] 
%\fw 
%\ctx{G}[\gpart{p}\to\gpart{q}:\{l_i\langle U_i\rangle.G_i \,;\, l_j\langle U_j\rangle.\past G_j\}_{i \in I\setminus j} ]}
\inferrule*[left=\fwcolor{(FVal1)}]{}
{\ctx{G}[ \past \gtcom{p}{q}{U}{G}] 
\fwg 
\ctx{G}[\gtcom{p}{\!\!\past q}{U}{G} ]}
\\
\inferrule*[left=\fwcolor{(FVal2)}]{}
{\ctx{G}[  \gtcom{p}{\!\!\past q}{U}{G}] 
\fwg 
\ctx{G}[\gtcom{p}{q}{U}{\past G} ]}
\\
\inferrule*[left=\fwcolor{(FCho1)}]{}
{
\begin{array}{c}
\ctx{G}[\past \gtcho{p}{q}{l_i}{G_i}] 
\qquad \qquad \qquad \qquad
\\
\qquad \qquad \quad
\fwg  
\ctx{G}[\gpart{p}\to\!\!\past\gpart{q}:\{\lbl_i:G_i \,;\, \lbl_j:G_j\}_{i \in I\setminus j} ] 
\end{array}
}
\\
\inferrule*[left=\fwcolor{(FCho2)}]{}
{
\begin{array}{c}
\ctx{G}[\gpart{p}\to\!\!\past\gpart{q}:\{\lbl_i:G_i \,;\, \lbl_j:G_j\}_{i \in I\setminus j} ] 
\qquad \qquad \qquad \quad
\\
\qquad \qquad
\fwg
\ctx{G}[\gpart{p}\to\gpart{q}:\{\lbl_i:G_i \,;\, \lbl_j:\past G_j\}_{i \in I\setminus j} ] 
\end{array}
}
\\
%%
\inferrule*[left=\bkcolor{(BVal1)}]{}
{\ctx{G}[\gtcom{p}{\!\!\past q}{U}{G} ]
\bkg
\ctx{G}[ \past \gtcom{p}{q}{U}{G}] 
}
\\
\inferrule*[left=\bkcolor{(BVal2)}]{}
{
\ctx{G}[\gtcom{p}{q}{U}{\past G} ]
\bkg
\ctx{G}[  \gtcom{p}{\!\!\past q}{U}{G}] 
}
\\
\inferrule*[left=\bkcolor{(BCho1)}]{}
{
\begin{array}{c}
\ctx{G}[\gpart{p}\to\!\!\past\gpart{q}:\{\lbl_i:G_i \,;\, \lbl_j:G_j\}_{i \in I\setminus j} ] 
\qquad \qquad
\\
\qquad \qquad
\bkg  
\ctx{G}[\past \gpart{p}\to\gpart{q}:\{\lbl_i:G_i \,;\, \lbl_j:G_j\}_{i \in I\setminus j} ]
\end{array}
}
\\
\inferrule*[left=\bkcolor{(BCho2)}]{}
{
\begin{array}{c}
\ctx{G}[\gpart{p}\to\gpart{q}:\{\lbl_i:G_i \,;\, \lbl_j:\past G_j\}_{i \in I\setminus j} ]
\qquad \qquad
\\
\qquad \qquad
\bkg 
\ctx{G}[\gpart{p}\to\!\!\past\gpart{q}:\{\lbl_i:G_i \,;\, \lbl_j:G_j\}_{i \in I\setminus j} ] 
\end{array}
}
%\\
%\inferrule[(RAct)]{\ctx{G'} [\bullet]= \ctx{G}[\gpart{p}\to\gpart{q}:\{l_i\langle U_i\rangle.G_i \,;\, l_i\langle U_j\rangle.\bullet\}_{i \in I\setminus j} ]}
%{
%\ctx{G'}[\past G_j] \bk 
%\ctx{G}[\past \gpart{p}\to\gpart{q}:\{l_i\langle U_i\rangle.G_i \,;\, l_i\langle U_j\rangle.G\}_{i \in I\setminus j} ]
%}
%\\
%\inferrule[(RAct1)]{ }
%{
%\ctx{G}[\gpart{p}\to\gpart{q}:\{l_i\langle U_i\rangle.G_i \,;\, l_j\langle U_j\rangle.\past G_j\}_{i \in I\setminus j} ]
%\bk
%\ctx{G}[\gpart{p}\to\!\past\gpart{q}:\{l_i\langle U_i\rangle.G_i \,;\, l_j\langle U_j\rangle.G_j\}_{i \in I\setminus j} ] 
%}
%\\
%\inferrule[(RAct2)]{ }
%{
%\ctx{G}[\gpart{p}\to\!\past\gpart{q}:\{l_i\langle U_i\rangle.G_i \,;\, l_j\langle U_j\rangle.G_j\}_{i \in I\setminus j} ]
%\bk
%\ctx{G}[ \past \gtact{p}{q}{l_i}{U_i}{G_i}] 
%}
\end{mathpar}
}
\vspace{-4mm}
\caption{Semantics of Global Types (Forward \& Backwards).\label{f:gts}}
\label{fig:prot_sem}
\end{figure}

syntax.tex
% !TEX root = revchor.tex

	\begin{figure}[t!]
	%{\small
		\begin{align*}
			u,w  \bnfis& n \bnfbar x,y,z
			\qquad \quad
			n,m \bnfis a,b \bnfbar \ep{s}{\p}%, \dual{s} 
			\\
			 {v},  {v}'  \bnfis &  \true \bnfbar \false \bnfbar \cdots
			\\
			V,W \bnfis & {a,b} \bnfbar  x,y,z \bnfbar  v, v' \bnfbar {\abs{x}{P}}
			\\%[1mm]
			P,Q
			 \bnfis &
			\bout{u}{V}{P}  \sbnfbar  \binp{u}{x}{P} \sbnfbar
			 \bsel{u}{\lbl_i. P_i}_{i\in I} \sbnfbar \bbra{u}{\lbl_i:P_i}_{i \in I}  
			 \\
			 & \sbnfbar  P \Par Q \sbnfbar  {\rvar{X} \sbnfbar \recp{X}{P}} 
						\sbnfbar  
			 {\appl{V}{u}}  
			\sbnfbar \news{n} P \sbnfbar \inact
\\
%M,N		 \bnfis &\inact \sbnfbar \np{\key{k}{i}}{P} \sbnfbar \moni{s} {H}{\mytilde{x}}{\store} \sbnfbar \mem{k}{(\appl{V}{u})}{k'}\sbnfbar M \Par N \sbnfbar \news{n} M\sbnfbar \coda{s}{h}\\
%
M,N		 \bnfis &\inact 
\sbnfbar 
\myloc{\loc}{\bout{a}{x}{P}}
\sbnfbar 
\myloc{\loc}{\binp{a}{x}{P}}
\sbnfbar 
M \Par N 
\sbnfbar 
\news{n} M
\\
& \sbnfbar 
\rtsyn{\np{\loc}{\conf{\stack C}{P}}} %% running process
\sbnfbar 
\rtsyn{\monig{s}{H}{\mytilde{x}}{\store}}  %% monitor
\\
& \sbnfbar 
\rtsyn{\codah{s}{h_i}{h_o}%{\restrict{\mytilde{\gpart{r}}}}
} % queue
\sbnfbar 
\rtsyn{\mem{k}{(\appl{V}{u})}{\loc}} % function
	\\
	\stack{C}, \stack{C}' \bnfis  & \inact \sbnfbar \bsel{u}{\lbl_i. P_i}_{i\in I} \sbnfbar 
\bbra{u}{ \lbl_i:P_i}_{i \in I} \sbnfbar \stack{C}_1, \stack{C}_2
\\
	\mytagg \bnfis & \rmark \sbnfbar \normark
	%	m \bnfis &\valueq{\p}{\q}{V} \sbnfbar \valueq{\p}{\q}{\lbl}  \sbnfbar m_1 \cons m_2 
%	\\
%	 h \bnfis & \emp   \sbnfbar h \cons m 
\qquad
	 h \bnfis  \emp   \sbnfbar h \cons \valueq{\p}{\q}{m} \qquad m \bnfis V \sbnfbar \lbl
\\[2mm]
%
    \alpha \bnfis &   \typeIn{\q}{U} \sbnfbar  \typeOut{\q}{U} 
    \\
	T,S		 \bnfis & \lend \sbnfbar	\alpha.S \sbnfbar \ltsel{\q}{\lbl_i}{S_i}{i}{I} \sbnfbar \ltbra{\q}{\lbl_i}{S_i}{i}{I}
	\\
	H,K		 \bnfis & \past S \sbnfbar S\past \sbnfbar \alpha_1.\cdots .\alpha_n.\past S 
	\\
	& \sbnfbar  
	\ltselp{\q}{\lbl_i:S_i \;;\; \lbl_j:H_j}{i}{I} \sbnfbar \ltbrap{\q}{\lbl_i:S_i \, , \, \lbl_j:H_j}{i}{I}
		\end{align*}
	%	}
		%\jp{We need to find a way of adding $\monir{s}{H}{\mytilde{x}}{\store}$ and $\codah{s}{h_i}{h_o}\restrict{\mytilde n,\p,\q}$.}
		\vspace{-4mm}
	\caption{\newjb{Syntax of processes $P, Q$, configurations $M, N$, 
	  stacks $\stack{C}, \stack{C}'$, 
	local types $T, S$, local types with history $H, K$.
    Constructs given in \rtsyn{\text{boxes}} appear only at run-time.}}
	\label{fig:syntax}
%	\vspace{-1mm}
\end{figure}

revchor-TR.bbl
\begin{thebibliography}{10}

\bibitem{DBLP:journals/jlp/AubertC17}
C.~Aubert and I.~Cristescu.
\newblock Contextual equivalences in configuration structures and
  reversibility.
\newblock {\em J. Log. Algebr. Meth. Program.}, 86(1):77--106, 2017.

\bibitem{DBLP:journals/fac/BarbaneraDd16}
F.~Barbanera, M.~Dezani{-}Ciancaglini, and U.~de'Liguoro.
\newblock Reversible client/server interactions.
\newblock {\em Formal Asp. Comput.}, 28(4):697--722, 2016.

\bibitem{DBLP:journals/tcs/BocchiCDHY17}
L.~Bocchi, T.~Chen, R.~Demangeon, K.~Honda, and N.~Yoshida.
\newblock Monitoring networks through multiparty session types.
\newblock {\em Theor. Comput. Sci.}, 669:33--58, 2017.

\bibitem{DBLP:journals/fac/CastellaniDP16}
I.~Castellani, M.~Dezani{-}Ciancaglini, and J.~A. P{\'{e}}rez.
\newblock Self-adaptation and secure information flow in multiparty
  communications.
\newblock {\em Formal Asp. Comput.}, 28(4):669--696, 2016.

\bibitem{CDYP2015}
M.~Coppo, M.~Dezani-Ciancaglini, L.~Padovani, and N.~Yoshida.
\newblock A gentle introduction to multiparty asynchronous session types.
\newblock In M.~Bernardo and E.~B. Johnsen, editors, {\em Formal Methods for
  Multicore Programming}, volume 9104 of {\em LNCS}, pages 146--178. Springer,
  2015.

\bibitem{DanosK04}
V.~Danos and J.~Krivine.
\newblock Reversible communicating systems.
\newblock In P.~Gardner and N.~Yoshida, editors, {\em {CONCUR} 2004}, LNCS,
  pages 292--307. Springer, 2004.

\bibitem{DBLP:conf/concur/DanosK05}
V.~Danos and J.~Krivine.
\newblock Transactions in {RCCS}.
\newblock In M.~Abadi and L.~de~Alfaro, editors, {\em {CONCUR} 2005}, pages
  398--412, 2005.

\bibitem{DBLP:journals/corr/Dezani-Ciancaglini16a}
M.~Dezani{-}Ciancaglini and P.~Giannini.
\newblock Reversible multiparty sessions with checkpoints.
\newblock In D.~Gebler and K.~Peters, editors, {\em {EXPRESS/SOS} 2016}, volume
  222 of {\em {EPTCS}}, pages 60--74, 2016.

\bibitem{Hennessy07}
M.~Hennessy.
\newblock {\em A {D}istributed {P}i-Calculus}.
\newblock CUP, 2007.

\bibitem{honda.vasconcelos.kubo:language-primitives}
K.~Honda, V.~T. Vasconcelos, and M.~Kubo.
\newblock Language primitives and type disciplines for structured
  communication-based programming.
\newblock In {\em ESOP'98}, volume 1381 of {\em LNCS}, pages 22--138. Springer,
  1998.

\bibitem{HYC08}
K.~Honda, N.~Yoshida, and M.~Carbone.
\newblock {Multiparty Asynchronous Session Types}.
\newblock In {\em POPL'08}, pages 273--284. ACM, 2008.

\bibitem{DBLP:journals/csur/HuttelLVCCDMPRT16}
H.~H{\"{u}}ttel, I.~Lanese, V.~T. Vasconcelos, L.~Caires, M.~Carbone,
  P.~Deni{\'{e}}lou, D.~Mostrous, L.~Padovani, A.~Ravara, E.~Tuosto, H.~T.
  Vieira, and G.~Zavattaro.
\newblock Foundations of session types and behavioural contracts.
\newblock {\em {ACM} Comput. Surv.}, 49(1):3:1--3:36, 2016.

\bibitem{KPY2016}
D.~Kouzapas, J.~A. P{\'{e}}rez, and N.~Yoshida.
\newblock On the relative expressiveness of higher-order session processes.
\newblock In P.~Thiemann, editor, {\em {ESOP} 2016}, pages 446--475, 2016.

\bibitem{DBLP:journals/mscs/KouzapasYHH16}
D.~Kouzapas, N.~Yoshida, R.~Hu, and K.~Honda.
\newblock On asynchronous eventful session semantics.
\newblock {\em Mathematical Structures in Computer Science}, 26(2):303--364,
  2016.

\bibitem{LaneseMS16}
I.~Lanese, C.~A. Mezzina, and J.~Stefani.
\newblock Reversibility in the higher-order {\(\pi\)}-calculus.
\newblock {\em Theor. Comput. Sci.}, 625:25--84, 2016.

\bibitem{DBLP:journals/eatcs/Lanese14}
I.~Lanese, C.~A. Mezzina, and F.~Tiezzi.
\newblock Causal-consistent reversibility.
\newblock {\em Bulletin of the {EATCS}}, 114, 2014.

\bibitem{DBLP:journals/corr/MezzinaP16}
C.~A. Mezzina and J.~A. P{\'{e}}rez.
\newblock Reversible sessions using monitors.
\newblock In D.~A. Orchard and N.~Yoshida, editors, {\em {PLACES} 2016}, volume
  211 of {\em {EPTCS}}, pages 56--64, 2016.

\bibitem{MezzinaP17}
C.~A. Mezzina and J.~A. P{\'{e}}rez.
\newblock Reversibility in session-based concurrency: A fresh look.
\newblock {\em J. Log. Algebr. Meth. Program.}, 2017.
\newblock To appear. Available in \url{http://jperez.nl}.

\bibitem{tlca07}
D.~Mostrous and N.~Yoshida.
\newblock Two session typing systems for higher-order mobile processes.
\newblock In {\em TLCA}, volume 4583 of {\em LNCS}, pages 321--335. Springer,
  2007.

\bibitem{SangiorgiD:expmpa}
D.~Sangiorgi.
\newblock {\em Expressing Mobility in Process Algebras: First-Order and Higher
  Order Paradigms}.
\newblock PhD thesis, University of Edinburgh, 1992.

\bibitem{DBLP:conf/concur/SangiorgiW01}
D.~Sangiorgi and D.~Walker.
\newblock On barbed equivalences in pi-calculus.
\newblock In K.~G. Larsen and M.~Nielsen, editors, {\em {CONCUR} 2001}, volume
  2154 of {\em LNCS}, pages 292--304. Springer, 2001.

\bibitem{DBLP:journals/jlp/TiezziY15}
F.~Tiezzi and N.~Yoshida.
\newblock Reversible session-based pi-calculus.
\newblock {\em J. Log. Algebr. Meth. Program.}, 84(5):684--707, 2015.

\bibitem{DBLP:conf/rc/TiezziY16}
F.~Tiezzi and N.~Yoshida.
\newblock Reversing single sessions.
\newblock In S.~J. Devitt and I.~Lanese, editors, {\em Reversible Computation -
  8th International Conference, {RC} 2016}, volume 9720 of {\em LNCS}, pages
  52--69. Springer, 2016.

\end{thebibliography}
