in coordinating the jobs over these worker nodes,
which is usually done as follows:

* Split the input data into chunks and delegate these chunks to worker
nodes, that each apply the “map” function $\mapvar$ to their given data in
parallel. We call these nodes the “mappers”.

* Collect the complete set of mapped results and “shuffle” them, group them by key.
The grouping is commonly implemented using a parallel sorting algorithm.

* Split the shuffled data into chunks and delegate these chunks to worker
nodes that each apply the “reduce” function $\redvar$ to their given
data in parallel. We call these nodes the “reducers”.

* Collect and aggregate the complete set of result of the reducers.

Our variant of the map-reduce model is defined as a function
$\vmapreducename\ n\ m\ \vmapvar\ \vredvar\ \loc$ in , which coordinates the work
for performing map-reduce on a linked list $\loc$ between $n$ mappers
applying the “map” function $\vmapvar$,
and $m$ reducers applying the “reduce” function $\vredvar$.
To make the implementation more interesting, we prevent storing intermediate
values locally by forwarding/returning them immediately as they are
The global structure is as follows:

* Start $n$ instances of the load-balancing
$\parmapperworkername$ from <Ref>,
parameterised with the $\vmapvar$ function, acting as the mappers.
Additionally start an instance of $\listsortelemservicename$ from
<Ref>, parameterised by a concrete comparison
function on the keys, corresponding to $\Lam (k_1,\_)\ (k_2,\_). k_1 < k_2$.
Note that the type of keys are restricted to be integers
for brevity's sake.

* Perform a loop that handles communication with the mappers.
If a mapper requests work, pop a value from the input list.
If a mapper returns work, forward it to the sorting service.
This process is repeated until all inputs have been mapped and forwarded.

* Start $m$ instances of the $\parmapperworkername$, parameterised by $\vredvar$, acting as the reducers.

* Perform a loop that handles communication with the mappers.
If a mapper requests work, group elements returned by the sort service.
If a mapper returns work, aggregate the returned value in a the linked
Grouped elements are created by requesting and aggregating elements from the
sorter until the key changes.

The aggregated linked list then contains the fully mapped input set upon

§.§ Functional correctness of map-reduce

The specification of the map-reduce program that we prove is as follows:

\[
\begin{array}{@{} l @{}}
\hoareV
\begin{array}{@{} l @{}}
0 < n\ *\
0 < m\ *\
\mapspecname\ \interpvar_\tvar\ \interpvar_\tvarZB\
\mapvar\ \vmapvar\ * \
\mapspecname\ \interpvar_\tvarZBs\
\interpvar_\tvarC\ \redvar\ \vredvar\ * \
\llistrefI{\interpvar_\tvar} \loc {\vec\var}
\end{array}
{\vmapreducename\ n\ m\ \vmapvar\ \vredvar\ \loc}
\Exists{\vec{\varC}}.
\vec{\varC} \equiv_p\ \mapreducename\ \mapvar\ \redvar\ \vec{\var} *
\llistrefI{\interpvar_\tvarC}{\loc}{\vec\varC}
\end{array}
\]

The $\mapspecname$ predicates (as introduced in <Ref>)
establish a connection between the functions $\mapvar$ and $\redvar$ in
Iris/and the functions $\vmapvar$ and $\vredvar$ in .
These make use of the various interpretation predicates $\interpvar_\tvar$,
$\interpvar_\tvarZB$, $\interpvar_{\tvarZBs}$, and $\interpvar_\tvarC$ for
the types in question.
Lastly, the $\llistrefI{\interpvar_\tvar} \loc {\vec\var}$ predicate determines
that the input is a linked list of the initial type $\tvar$.
The postcondition asserts that the result $\vec \varC$ is a permutation of the
original linked list $\vec \var$ applied to the functional specification
$\mapreducename$ of map-reduce from <Ref>.

§ THE MODEL OF

We construct a model of as a shallow embedding in
the Iris framework [51, 50, 48, 49].
This means that the type $\iProto$ of ,
the subprotocol relation $\subprot{\prot_1}{\prot_2}$,
and the connective $\interp \chan \prot$ for the channel ownership,
are definitions in Iris,
and the proof rules are lemmas about these definitions in Iris.

In this section we describe the relevant aspects of the model of .
We model the type $\iProto$ of as the solution of a recursive domain equation, and
describe how the operations for dual and composition are defined
We then define the subprotocol relation $\subprot {\prot_1} {\prot_2}$
and prove its proof rules as lemmas (<Ref>).
To connect protocols to the endpoint channel buffers in the semantics
we define the protocol consistency relation,
which ensures that a pair of protocols is consistent with the messages in
their associated buffers (<Ref>).
On top of the protocol consistency relation, we define the ghost theory for
which forms the key ingredient for defining the connective $\interp\chan\prot$ for
channel ownership (<Ref>) that links protocols to the
semantics of channels (<Ref>).
We then show how adequacy follows from the embedding in Iris (<Ref>).
Finally, we show how to solve the recursive domain equation for the type
$\iProto$ of (<Ref>).

§.§ The model of

To construct a model of , we first need to determine what they mean
The challenging part involves the constructors
$\sendprot{\xdots}{\val}{\iprop}{\prot}$ and
$\recvprot{\xdots}{\val}{\iprop}{\prot}$, whose (higher-order and
impredicative) $\xdots$ bind into the communicated value $\val$, the
transferred resources $\iprop$, and the tail protocol $\prot$.
We model these constructors as predicates over the communicated value
and the tail protocol.
To describe the transferred resources $\iprop$, we model these protocols as
Iris predicates (functions to $\iProp$).
This gives rise to the following recursive domain equation:

\begin{align*}
\newaction \bnfdef{}& \actionsend \mid \actionrecv\\
\iProto \cong{}&
1 + (\newaction \times (\Val \to \latert \iProto \to \iProp))
\intertext{The left part of the sum type (the unit type $\unit$) indicates that
the protocol has terminated, while the right part describes a message that is
exchanged, expressed as an Iris predicate.
Since the recursive occurrence of $\iProto$ in the predicate appears in negative
we guard it using Iris's \emph{type-level later} ($\latert$) operator (whose only
constructor is $\latertinj : \tvar \to \latert\ \tvar$).
The exact way the solution is constructed is detailed in
\Cref{sec:equation_solution}.
For now, we assume a solution exists, and define the \pname constructors as:}
\protend \eqdef{}& \Inj 1 \TT \\
\sendprot{\xdots}{\val}{\iprop}{\prot} \eqdef{}&
\Inj 2 (\actionsend, \Lam \valB\,\prot'.
\Exists \xdots. (\val = \valB) * \iprop * (\prot' = \latertinj\ \prot)) \\
\recvprot{\xdots}{\val}{\iprop}{\prot} \eqdef{}&
\Inj 2 (\actionrecv, \Lam \valB\,\prot'.
\Exists \xdots. (\val = \valB) * \iprop * (\prot' = \latertinj\ \prot))
\end{align*}

The definitions of $\sendprot{\xdots}{\val}{\iprop}{\prot}$ and
$\recvprot{\xdots}{\val}{\iprop}{\prot}$ make use of the (higher-order and
impredicative) existential quantifiers of Iris
to constrain the actual message $\valB$ and tail $\prot'$ so that they agree
with the message $\val$ and tail $\prot$ prescribed by the protocol.

Recursive protocols.

Iris's guarded recursion operator $\MU \var. \term$ requires the
recursion variable $\var$ to appear under a contractive term construct in $\term$.
Hence, to use Iris's recursion operator to construct recursive protocols, it is
essential that the protocols $\sendprot{\xdots}{\val}{\iprop}{\prot}$ and
$\recvprot{\xdots}{\val}{\iprop}{\prot}$ are contractive in the tail $\prot$.
To show why this is the case, let us first define what it means for a function
$f : \tvar \to \tvarB$ to be contractive:

\[
\All \var,\varB. \later(\var = \varB) \Ra f\; \var = f\; \varB
\]

Examples of contractive functions are the later modality
$\later : \iProp \to \iProp$ and the constructor $\latertinj : \tvar \to \latert\ \tvar$.
The protocols $\sendprot{\xdots}{\val}{\iprop}{\prot}$ and
$\recvprot{\xdots}{\val}{\iprop}{\prot}$ are defined so that
$\prot$ appears below a $\latertinj$, and hence we can prove
that they are contractive in $\prot$.

With these definitions at hand, the dual $\dual{(\_)}$ and append
$(\protapp {\_} {\_})$ operations are defined using Iris's guarded
recursion operator ($\MU \var.\term$):

\begin{align*}
\dual{(\_)} \eqdef{}&
\MU \recvar. \Lam \prot.
\begin{cases}
\Inj 1 \TT
& \textnormal{if } \prot = \Inj 1 \TT \\
\Inj 2 (\dual a,
\begin{array}[t]{@{} l @{}}
\Lam \valB\ \prot'. \Exists \prot''. \\ \quad
\begin{array}[t]{@{} l @{}}
\pred\ \valB\ (\latertinj\ \prot'')\ \ast \\
\prot' = \latertinj\ (\recvar\ \prot''))
\end{array}\end{array}
& \textnormal{if } \prot = \Inj 2 (a, \pred)
\end{cases} \\
(\protapp{\_}{\prot_2}) \eqdef{}&
\MU \recvar. \Lam \prot_1.
\begin{cases}
\prot_2
& \textnormal{if } \prot_1 = \Inj 1 \TT \\
\Inj 2 (a,
\begin{array}[t]{@{} l @{}}
\Lam \valB\ \prot'. \Exists \prot''. \\ \quad
\begin{array}[t]{@{} l @{}}
\pred\ \valB\ (\latertinj\ \prot'')\ \ast \\
\prot' = \latertinj\ (\recvar\ \prot''))
\end{array} \end{array}
& \textnormal{if }\prot_1 = \Inj 2 (a, \pred)
\end{cases}
\end{align*}

In the above definitions, we let $\dual{\actionsend} \eqdef{} \actionrecv$
and $\dual{\actionrecv} = \actionsend$.

The base cases of both definitions are as expected.
In the recursive cases, we construct a new predicate, given the original
predicate $\pred$.
In these new predicates, we quantify over an original tail protocol $\prot''$ such
that $\pred\ \valB\ (\latertinj\ \prot'')$ holds, and unify the new tail
protocol $\prot'$ with the result of the recursive call $\recvar\ \prot''$.

The equational rules for dual $\dual{(\_)}$ and append $(\protapp {\_} {\_})$ from
<Ref> are proven as lemmas in Iris using Loeb induction.
This is possible as the recursive call $\recvar\ \prot''$ appears below a
$\latertinj$ constructor—since the $\latertinj$ constructor is contractive, we can
strip-off the later from the induction hypothesis when proving the equality for
the tail.

Difference from the conference version.

In the conference version of this paper [35],
we described two versions of the recursive domain equation for :
an “ideal” version (as used in this paper), where $\iProto$ appears in negative
position, and an “alternative” version, where $\iProto$ appears in positive
At that time, we were unable to construct a solution of the “ideal”
version, so we used the “alternative” version.
In <Ref> we show how we are now able to solve the “ideal”

In the conference version of this paper, the proposition $\iprop$
appeared under a later modality in the definitions of the protocols
$\sendprot{\xdots}{\val}{\iprop}{\prot}$ and $\recvprot{\xdots}{\val}{\iprop}{\prot}$,
making these protocols contractive in $\iprop$.
This choice was motivated by the ability to construct recursive protocols like
$\MU \recvar. \sendprot{(\chan:\Val)}{\chan}{\interp \chan \prot}{\prot'}$,
where the payload refers to the recursion variable $\recvar$.
In the current version (without the later modality) we can still construct such
protocols, because $\interp \chan \prot$ is contractive in $\prot$.
We removed the later modality because it is incompatible with the rules SP-send-elim
and SP-recv-elim for subprotocols.

§.§ The model of the subprotocol relation

We now model the subprotocol relation $\subprot {\prot_1} {\prot_2}$ from
For legibility, we present it in the style of an inference system through its
constructors, whereas it is formally defined using Iris's
guarded recursion operator ($\MU \var.\term$):

1  1

_2    (  _2)

_1    (  _1) ∗

(_1 _2)

2 (,_1)2 (,_2)

_1   (  _1)

_2.     _2    (  _2) ∗

(_1 _2)

2 (,_1)2 (,_2)

(_1 _1 ( _1) ∗_2 _2 ( _2))

) ∗(

2 (,_1)2 (,_2)

To be a well-formed guarded recursion definition, every
recursive occurrence of $\subprotop$ is guarded by the later modality ($\later$).
Aside from later being required for well-formedness,
these laters make it possible to reason about
the subprotocol relation using Loeb induction; both to prove the
subprotocol rules from <Ref> as lemmas, and for users to
reason about recursive protocols as shown in <Ref>.
The relation is defined in a syntax directed fashion (there are no overlapping rules), and therefore all constructors need to be
defined so that they are closed under monotonicity and transitivity.

The first constructor states that terminating protocols ($\protend \eqdef
\Inj 1 \TT$) are related.
The other constructors concern the protocols
$\sendprot{\xdots}{\val}{\iprop}{\prot}$ and
$\recvprot{\xdots}{\val}{\iprop}{\prot}$, which are modelled
as $\Inj 2 {(\actionsend,\pred)}$ and $\Inj 2 {(\actionrecv,\pred)}$, where
$\pred : \Val \to \latert \iProto \to \iProp$
is a predicate over the communicated value and tail protocol.
While the actual constructors are somewhat intimidating because they are defined
in terms of these predicates in the model, they
essentially correspond to the following high-level versions:

. _2 .
(_1 = _2) * _1 *
(_1 _2)
_1 _1 _1
_2 _2 _2
. _1 .
(_1 = _2) * _2 *
(_1 _2)
_1 _1 _1
_2 _2 _2
,. (_1 * _2) .
(_1  _2 ) *
( _1  _2)

_1 _1 _1
_2 _2 _2

To obtain syntax directed rules, the first rule combines SP-send-elim,
SP-send-intro, and SP-send-mono, and dually, the second
rule combines SP-recv-elim, SP-recv-intro, and
The third rule combines SP-recv-elim, SP-send-elim and
SP-swap and bakes in transitivity, instead of asserting
that $\prot_1$ and $\prot_2$ are equal to $\sendprotT {} {\val_2} {\prot}$ and
$\recvprotT {} {\val_1} {\prot}$, respectively.

The rules from the beginning of this section are defined by generalising
the high-level rules to arbitrary predicates.
For example, rule $\subprot{\Inj 2 {(\actionsend,\pred_1)}}{\Inj 2 {(\actionsend,\pred_2)}}$
requires that for any value $\val$ and tail protocol $\prot_2$ that
are allowed by the predicate $\pred_2$, there is a stronger tail protocol $\prot_1$
(where $\subprot {\prot_1} {\prot_2}$),
so that the same value $\val$ and stronger tail protocol
$\prot_1$ are allowed by the predicate $\pred_1$.

The rules in <Ref> on page fig:subprotocol_rules
are proven as lemmas.
Those for and resource manipulation (SP-send-elim,
SP-send-intro, SP-recv-elim and SP-recv-intro),
monotonicity (SP-send-mono and SP-recv-mono),
and swapping (SP-swap) follow
almost immediately from the definition, whereas
those for reflexivity (SP-refl), transitivity (SP-trans),
and the dual and append operator (SP-dual and SP-append)
are proven using Loeb induction.

§.§ Protocol consistency

To connect to the semantics of channels in <Ref>, we define
the protocol consistency relation $\proteval \vsl \vsr {\prot_1} {\prot_2}$,
which expresses that protocols $\prot_1$ and $\prot_2$ are consistent
w.r.t. channel buffers containing values $\vsl$ and $\vsr$.
The consistency relation is defined as:

\begin{align*}
\proteval \vsl \vsr {\prot_1} {\prot_2}
\eqdef{}& \Exists \prot. \\
& \hspace{-13em}
(\subprot {\recvprotT {} {\vec\val_{2.1}} {\dots
\recvprotT {} {\vec\val_{2.\listlength{\vsr}}} \prot}} {\prot_1}) *
(\subprot {\recvprotT {} {\vec\val_{1.1}} {\dots
\recvprotT {} {\vec\val_{1.\listlength{\vsl}}} {\dual\prot}}} {\prot_2})
\end{align*}

Intuitively, $\proteval \vsl \vsr {\prot_1} {\prot_2}$
ensures that for all messages
$\vsl = \vec\val_{1.1} \dotsc \vec\val_{1.\listlength{\vsl}}$ in transit from the endpoint described
by $\prot_1$ to the endpoint described by $\prot_2$, the protocol $\prot_2$ is
expecting to receive these message in order (and for $\vsr$),
after which the remaining protocols $\prot$ and $\dual\prot$ are dual.
To account for weakening we close the consistency relation under subprotocols
(by using $\subprotop$ instead of equality).
Closure under the subprotocol relation additionally implicitly captures ownership of the
quantifiers and resources associated with the messages $\vsl$ and $\vsr$.
That is, since the subprotocol relations relate the protocol arguments
$\prot_1$ and $\prot_2$ with protocols that specify no quantifiers or resources.
More precisely, by the definition of the subprotocol relation
(shown in <Ref>), a relation such as
$\recvprotT{}{\val}{}{\prot_1} \subprotop \recvprot{(\xdots)}{\val}{\iprop}{\prot_2}$
is equivalent to a separation implication of the form
$\TRUE \wand \Exists \xdots. \iprop \ast \later \prot_1 \subprotop \prot_2$,
where the obligation $\TRUE$ is trivial, meaning that it implicitly asserts
ownership of $\iprop$.

Finally, closure under the subprotocol relation gives that
$\proteval \vsl \vsr {\prot_1} {\prot_2}$ and $\subprot {\prot_1} {\prot_1'}$
implies $\proteval \vsl \vsr {\prot_1'} {\prot_2}$,
and ensures that the consistency relation enjoys the following rules
corresponding to creating a channel, sending a message, and receiving a message:

\begin{align*}
& \proteval \nil \nil {\prot} {\dual \prot}
\\[0.5em]
& \begin{array}{@{} l @{}}
(\proteval \vsl \vsr {(\sendprot \xdots \val \iprop {\prot_1})} {\prot_2}
\ast \subst \iprop {\vec\var} {\vec\term}) \wand \\
\qquad
\lateropt {\listlength \vsr} (
\proteval {(\snoc {\subst \val {\vec\var} {\vec\term}} \vsl)} \vsr {\prot_1} {\prot_2})
\end{array} \\[0.5em]
& \begin{array}{@{} l @{}}
\proteval \vsl {(\cons \valB \vsr)} {(\recvprot \xdots \val \iprop {\prot_1})} {\prot_2}
\wand \\
\qquad
\Exists \vec\varB.
(\valB = \subst \val {\vec\var} {\vec\varB}) *
\subst \iprop {\vec\var} {\vec\varB} \ast
\later (\proteval \vsl \vsr {\prot_1} {\prot_2})
\end{array}
\end{align*}

The first rule states that dual protocols are consistent w.r.t. a pair of
empty buffers.
The second rule states that a protocol $\sendprot \xdots \val \iprop {\prot_1}$
can be advanced to $\prot_1$ by giving up ownership of
$\subst \iprop {\vec\var} {\vec\term}$ and enqueueing the value
$\subst \val {\vec\var} {\vec\term}$ in the buffer $\vsl$.
Dually, the third rule states that given a protocol
$\recvprot \xdots \val \iprop {\prot_1}$ and a buffer that contains value
$\valB$ as its head, we learn that $\valB$ is equal to
$\subst \val {\vec\var} {\vec\varB}$, and that we can obtain ownership of
$\subst \iprop {\vec\var} {\vec\varB}$ by advancing the protocol to $\prot_1$
and dequeuing the value $\valB$ from the buffer.
Since the relation is symmetric, if $\proteval \vsl \vsr {\prot_1} {\prot_2}$
then $\proteval \vsr \vsl {\prot_2} {\prot_1}$, we obtain similar rules for
the protocol $\prot_2$ on the right-hand side.

The last two rules are proven by case analysis on the subprotocol relation
($\subprotop$) in the assumption.
Since the subprotocol relation ($\subprotop$) is defined using guarded recursion,
we obtain a later modality ($\later$) for each case analysis.
To prove the first of the rules, we need to perform a number of case analyses
equal to the size of the buffer $\vsr$,
whereas for the second rule we need to perform just a single case analysis.
These later modalities are eliminated through the $\SkipN$ operation in
the $\sendname$ operation, see
<Ref> for further discussion.

§.§ The ghost theory

To provide a general interface for making 's reasoning principles
independent of ,
we employ a standard ghost theory approach in Iris to compartmentalise channel
In <Ref> we define the connective $\interp \chan \prot$
for channel endpoint ownership that links the ghost theory to the buffers of
our implementation of channels in .

The ghost theory is similar in its interface to the ghost theory for
contributions that we used in <Ref>.
We define three new logical connectives—an authority
$\protoctx{\gpname}{\vsl}{\vsr}$, and tokens
$\protofragleft{\gpname}{\prot_l}$ and
$\protofragright{\gpname}{\prot_r}$—and prove rules about how they can be
allocated, updated, and used.
Similar to prior ghost theories, the identifier
$\gpname$ associates the connectives to each other.
The $\protoctx{\gpname}{\vsl}{\vsr}$ connective can be thought of as
an authority that governs the global state of the buffers $\vsl$ and $\vsr$.
The tokens $\protofragleft{\gpname}{\prot_l}$ and
$\protofragright{\gpname}{\prot_r}$ provide local views of the buffers state
in terms of the protocols $\prot_l$ and $\prot_r$.
As we will see in <Ref>, the authority can be shared
using a lock, while the tokens provide unique ownership of each endpoint.

To define the connectives of the ghost theory
we use Iris's existing ghost theory for higher-order ghost variables,
revolving around the two connectives
$\gname \mapsto_{\authfull} \prot$ and $\gname \mapsto_{\authfrag} \prot'$,
which we call the inner and outer fragments, respectively.
As before, the $\gname$ is the ghost identifier that associates the connectives.
The fragments can be thought of as two pieces of a single variable,
which can only be updated in the presence of both fragments.
As a result, we know that inner and outer fragment with the same ghost identifier
$\gname$ always point to the same protocol $\prot$.
This is made precise by the rules as shown in <Ref>.
In particular, higher-order ghost variables are allocated in pairs
$\gname \mapsto_{\authfull} \prot$ and
$\gname \mapsto_{\authfrag} \prot$ for an identical protocol $\prot$
and they can only be updated together (ho-ghost-update).
This means that they will always hold the same protocol
The subtle part of the higher-order ghost variables is that they involve ownership
of a protocol of type $\iProto$, which is defined in terms of Iris propositions
Due to the dependency on $\iProp$ (which is covered in detail in
<Ref>) the rule ho-ghost-agree only gives the
equality between the protocols under a later modality ($\later$).

With Iris's higher-order ghost variables at hand, we can define the ghost theory
connectives as:

\begin{align*}
\protoctx{(\gnamel, \gnamer)}{\vsl}{\vsr} \eqdef{}&
\Exists \prot_1, \prot_2.
\begin{array}[t]{@{} l @{}}
\gnamel \mapsto_{\authfull} \prot_1 \ast
\gnamer \mapsto_{\authfull} \prot_2\ \ast\\
\later \proteval \vsl \vsr {\prot_1} {\prot_2}
\end{array}\\
\protofragleft{(\gnamel, \gnamer)}{\prot_l} \eqdef{}&
\Exists \prot_l'.
\gnamel \mapsto_{\authfrag} \prot_l' \ast
\later (\subprot{\prot_l'}{\prot_l})
\\
\protofragright{(\gnamel, \gnamer)}{\prot_r} \eqdef\ &
\Exists \prot_r'.
\gnamer \mapsto_{\authfrag} \prot_r' \ast
\later (\subprot{\prot_r'}{\prot_r})
\end{align*}

Since we use two higher-order ghost variables,
our identifiers $\gpname \bnfdef (\gnamel, \gnamer)$
are pairs of Iris ghost identifiers.
The authority $\protoctx{(\gnamel, \gnamer)}{\vsl}{\vsr}$
asserts ownership of the inner fragments of the higher-order ghost
$\gnamel \mapsto_{\authfull} \prot_1$ and $\gnamer \mapsto_{\authfull} \prot_2$
for some protocols $\prot_1$ and $\prot_2$.
It then asserts that the buffers $\vsl$ and $\vsr$ are consistent with respect to
those protocols $\prot_1$ and $\prot_2$
(via $\proteval{\vsl}{\vsr}{\prot_1}{\prot_2}$).
The tokens
$\protofragleft{(\gnamel, \gnamer)}{\prot_l}$ and
$\protofragright{(\gnamel, \gnamer)}{\prot_r}$ respectively
assert ownership of the outer higher-order ghost variable fragments
$\gnamel \mapsto_{\authfrag} \prot_l'$ and $\gnamer \mapsto_{\authfrag} \prot_r'$.
Here $\prot_l'$ and $\prot_r'$ are protocols that are weaker than the protocol
arguments $\prot_l$ and $\prot_r$ (via $\subprot{\prot'_l}{\prot_l}$ and
The explicit weakening under the subprotocol relation may seem redundant,
as weakening is already accounted for in $\protevalname$.
However, it allows us to weaken the
protocols of the tokens without the presence of the authority as
shown momentarily.
The later modality ($\later$) makes sure that $\protofragleft{(\gnamel, \gnamer)} \prot$
and $\protofragright{(\gnamel, \gnamer)} \prot$ are contractive in $\prot$.

With the definitions of the ghost theory connectives at hand,
we prove the rules of the ghost theory presented in
The rule proto-alloc corresponds to allocation of a buffer pair, the rules
proto-send-l and proto-send-r correspond to sending a
message, and the rules proto-recv-l and proto-recv-r
correspond to receiving a message.
Finally, the rules proto-weaken-l and proto-weaken-r captures
that we can weaken the protocols of the tokens without the presence of the
The rules of <Ref> are proven through a combination of
the rules for higher-order ghost
state from <Ref>, and the rules for the protocol consistency
relation $\protevalname$ from <Ref>.

§.§ The model of channel ownership

To link the physical contents of the bidirectional channel $\chan$ to the
ghost theory we define the channel ownership connective as follows:

\begin{align*}
\interp \chan \prot \eqdef{}&
\Exists \gpname,l,r,\lockvar.
\begin{array}[t]{@{} l}
\left(\begin{array}{@{} l @{}}
(\chan = (l,r,\lockvar) * \protofragleft{\gpname}{\prot})\ \lor\\
(\chan = (r,l,\lockvar) * \protofragright{\gpname}{\prot})
\end{array}\right) \ast\\
\islock \lockvar
{(\Exists \vec\val_1\,\vec\val_2.
\llistref{l}{\vec\val_1} \ast
\llistref{r}{\vec\val_2} \ast
\protoctx{\gpname}{\vec\val_1}{\vec\val_2})}\
\end{array}
\end{align*}

The predicate states that the referenced channel endpoint $\chan$
is either the left $(l,r,\lockvar)$ or the right $(r,l,\lockvar)$ side of a channel,
and that we have exclusive ownership of the ghost token
$\protofragleft{\gpname}{\prot}$ or $\protofragright{\gpname}{\prot}$ for the
corresponding side.
Iris's lock representation predicate $\logdefemph{is\_lock}$
(previously presented in <Ref>) is used to make sharing of the
buffers possible.
The lock invariant is governed by lock $\lockvar$, and carries
the ownership $\llistref{l}{\vec\val_1}$
and $\llistref{r}{\vec\val_2}$ of the mutable linked lists containing the channel
buffers, as well as $\protoctx{\gpname}{\vec\val_1}{\vec\val_2}$, which
asserts protocol consistency of the buffers with respect to the protocols.

With the definition of the channel endpoint ownership along with the ghost theory and
lock rules we then prove the channel rules Ht-new,
Ht-send and Ht-recv from <Ref>.
The proofs are carried out through symbolic execution to the point
where the critical section is entered, after which the rules of the ghost theory
(<Ref>) are used to allocate or update the ghost state appropriately so that it matches
the physical channel buffers.

The need for skip instructions.

The rules proto-send-l and proto-send-r from
<Ref> contain a number of later modalities ($\later$)
proportional to the other endpoint's buffer.
As explained in <Ref> these later modalities are the consequence
of having to perform a number of case analyses on the subprotocol relation,
which is defined using guarded recursion, and thus contains a later modality
for each recursive unfolding.

To eliminate these later modalities, we instrument the code of the function with the $\SkipN\ (\llistlength\ r)$ instruction, which performs a number
of skips equal to the size of the other endpoint's buffer $r$.
The $\SkipN$ instruction has the following specification:

\[
\textstyle\hoare{\later^{n}\iprop}{\SkipN\ n}{\iprop}
\]

Instrumentation with skip instructions is used often in work on step-indexing,
see  [74, 32].
Instrumentation is needed because current step-indexed logics like Iris
unify physical/program steps and logical steps, for
each physical/program step at most one later can be eliminated from the hypotheses.
In recent work by
Svendsen  [74],
Matsushita and Jourdan [61], and Spies  [72]
more liberal versions of step-indexing have been proposed, but none of these
versions of step-indexing have been integrated into the main Coq development of Iris and .

§.§ Adequacy of

Having constructed the model of in Iris,
we obtain the following main result,
as first presented in <Ref>:

Let $\fpred \in \Val \to \mProp$ be a meta-level (Coq) predicate over values and
suppose $\hoare \TRUE \expr {\Ret \val. \fpred\ \val}$ is
derivable in Iris, then
$\safe{\expr}$ and

Since is an internal logic embedded in Iris, the proof is an immediate
consequence of Iris's adequacy theorem

§.§ Solving the recursive domain equation for protocols

Recall the recursive domain equation for from <Ref>:

\[
\iProto \cong{}
1 + (\newaction \times (\Val \to \latert \iProto \to \iProp))
\]

This recursive domain equation shows that $\iProto$ depends on the type $\iProp$
of Iris propositions.
To use types that depend on $\iProp$ as part of higher-order ghost state in Iris,
such types need to be bi-functorial in $\iProp$.
Hence, this means that to construct $\iProto$, in a way that it can be used
in combination with the higher-order ghost variables in <Ref>,
we need to solve the following recursive domain equation:

\[
\iProto(\Pneg,\Ppos) \cong{}
1 + (\newaction \times (\Val \to \latert \iProto(\Ppos,\Pneg) \to \Ppos))
\]

Since the recursive occurrence of $\iProto$ appears in negative position, the
polarity needs to be inverted for $\iProto$ to be bi-functorial.

The version of Iris's recursive domain equation solver based
on [6, 14] as mechanised in Iris's Coq
development is not readily able to construct a solution of $\iProto(\Pneg,\Ppos)$.
Concretely, the solver can only construct solutions of non-parameterised
recursive domain equations.
While a general construction for solving such recursive domain
equations exists <cit.>, that construction has not been
mechanised in Coq.
We circumvent this shortcoming by solving the following recursive domain
equation instead, in which we unfold the recursion once by hand:

\[\begin{array}{@{}l@{}}
\iProto_2(\Pneg,\Ppos) \cong{}\\
\quad
\begin{array}{@{}l@{}}
1 + \Big(\newaction \times \big(\Val \to
\latert (1 + (\newaction \times
(\Val \to \latert \iProto_2(\Pneg,\Ppos)\to \Pneg))) \to
\Ppos\big)\Big)
\end{array}
\end{array}\]

Here, the polarity in the recursive occurrence is fixed, allowing us to solve
$\iProto_2(\Pneg,\Ppos)$ using Iris's existing recursive domain equation solver.
This is sufficient because a solution of $\iProto_2(\Pneg,\Ppos)$ is isomorphic
to a solution of $\iProto(\Pneg,\Ppos)$.

§ COQ MECHANISATION

The definition of the logic, its model, and the proofs of all examples
in this paper have been fully mechanised using the Coq proof
assistant [18].
In this section we will elaborate on the mechanisation effort
(<Ref>), and go through the full proof of a message-passing program
(<Ref>) and a subprotocol relation (<Ref>)
showcasing the tactics for .
We display proofs and proof states taken directly from the Coq
mechanisation, which differ in notation from the paper as shown in <Ref>.

Notation on paper     Notation in Coq
$\sendprot{\var_1 \ldots \var_n}{\val}{\iprop}\prot$
|<! x_1 .. x_n> MSG v  P ; prot|

$\recvprot{\var_1 \ldots \var_n}{\val}{\iprop}\prot$
|<? x_1 .. x_n> MSG v  P ; prot|

|iProto_dual prot|

$\TT$, $5$, $\True$
|#()|, |#5|, |#true|

$\var$, $\varB$, $\varC, \_$
|"x"|, |"y"|, |"z"|, |<>|

$1$, $\nat$, $\integer$
|()|, |nat|, |Z|

Overview of notations in the Coq mechanisation.

§.§ Mechanisation effort

The mechanisation of is built on top of the mechanisation of Iris
[51, 48, 49].
To carry out proofs in separation logic, we use the MoSeL Proof Mode
(formerly Iris Proof Mode) [55, 52], which
provides an embedded proof assistant for separation logic in Coq.
Building on top of the Iris and MoSeL framework in Coq has a number of tangible

* By defining channels on top of ,
we do not have to define a full programming language
semantics, and can reuse all of the program libraries and Coq machinery,
including the tactics for symbolic execution of non message-passing programs.

* Since is mechanised as an Iris library
we get all of the features of Iris for free,
such as the ghost state mechanisms for reasoning about concurrency.

* When proving the proof rules, we can make use of the MoSeL Proof
Mode to carry out proofs directly using separation logic, thus reasoning at
a high level of abstraction.

* We can make use of the extendable nature of the MoSeL Proof Mode to
define custom tactics for symbolic execution of message-passing programs.

These advantages made it possible to mechanise , along with the examples of
the paper, with a small Coq development of a
total size of about 5000 lines of code (comments and whitespace included).
The line count of the different components are shown in <Ref>.

§.§ Tactic support for session type-based reasoning

To carry out interactive proofs using symbolic execution, we follow the
methodology described in the original Iris Proof Mode paper [55].
In particular, this means that the logic in Coq is presented in weakest precondition
style rather than using Hoare triples.
For handling or we define the following tactics:

|wp_send (t1 .. tn)$\! $ with "[H1 .. Hn]"|   and   |wp_recv (y1 .. yn)$\! $ as "H"|.

These tactics roughly perform the following actions:

* Find a or in evaluation position of the program
under consideration.

* Find a corresponding $\interp \chan \prot$ hypothesis in the separation
logic context.

* Normalise the protocol $\prot$ using the rules for duals, composition,
recursion, and swapping so it has a
$\sendprot {\xdots} \val \iprop \prot$ or
$\recvprot {\xdots} \val \iprop \prot$ construct in its head position.

* In case of |wp_send|, instantiate the variables $\xdots$ using
the terms |(t1 .. tn)|, and create a goal for the proposition
$\iprop$ with the hypotheses |[H1 .. Hn]|.
Hypotheses prefixed with $\mathtt{\$}$ will automatically be consumed to resolve a
subgoal of $\iprop$ if possible.
In case the terms |(t1 .. tn)| are omitted, an attempt is made to
determine these using unification.

* In case of |wp_recv|, introduce the variables $\xdots$ into the
context by naming them |(y1 .. yn)|, and create a hypothesis
|H| for $\iprop$.

The implementation of these tactics follows the approach by Krebbers  [55].
The protocol normalisation is implemented via logic programming with type

As an example we will go through a proof of the following program:

\[
\begin{array}[t]{@{} l @{\ } l @{}}
\mathtt{prog\_ref\_swap\_loop} \langdef{}
\Lam \_. &
\LetNoIn {\chan} = \start
(\Rec {\mathit{go}} \chan' =
\begin{array}[t]{@{} l @{}}
\Let l = {\recv \chan'} in \\
l \leftarrow \deref l + 2; \\
\send {\chan'} \TT;\ \mathit{go}\ \chan')\ \In \\
\end{array}\\
& \Let {l_1} = \newref 18 in \Let {l_2} = \newref 20 in\\
& \send \chan l_1;\ \send \chan l_2; \\
& \recv \chan;\ \recv \chan;\\
& \deref l_1 + \deref l_2
\end{array}
\]

Here, the forked-off thread acts as a service that recursively receives locations,
adds 2 to their stored number, and then sends back a flag indicating that the
location has been updated.
The main thread, acting like a client, first allocates two new references,
to $18$ and $20$, respectively, which are both sent to the service
after which the update flags are received.
It finally dereferences the updated locations, and adds their values together,
thus returning $42$.
To verify this program, we use the following recursive protocol:

\[
\mathtt{prot\_ref\_loop} \eqdef \MU (\recvar:\iProto).
\sendprot{(\loc : \Loc) (\var : \integer)}{\loc}{\loc \mapsto \var}
\recvprot{}{\TT}{\loc \mapsto \var+2}
\recvar
\]

The (forked-off) service follows the (dual of) the protocol exactly,
while the main thread follows a weakened version.
The recursion is unfolded
twice, after which the second send has been swapped ahead of the first receive,
allowing it to first send both values before receiving:

\[
\begin{array}{@{} l @{\ } l}
\mathtt{prot\_ref\_loop}
\subprotop
&\begin{array}[t]{@{} l}
\sendprot{(\loc_1:\Loc)(\var_1:\integer)}{\loc_1}{\loc_1 \mapsto \var_1} \\
\sendprot{(\loc_2:\Loc)(\var_2:\integer)}{\loc_2}{\loc_2 \mapsto \var_2} \\
\recvprot{}{\TT}{\loc_1 \mapsto (\var_1+2)} \\
\recvprot{}{\TT}{\loc_2 \mapsto (\var_2+2)}
\mathtt{prot\_ref\_loop}
\end{array}
\end{array}
\]

The full Coq proof of the program is shown in <Ref>.

Lemma prog_ref_swap_loop_spec : ∀ Φ, Φ$\ $#42 -∗ WP prog_ref_swap_loop #()  Φ$\ $.
iIntros (Φ) "HΦ". wp_lam. ||
wp_apply (start_chan_spec prot_ref_loop); iIntros (c) "Hc". ||
- iLöb as "IH". wp_lam. ||
wp_recv (l x) as "Hl". wp_load. wp_store. wp_send with "[$\$$Hl]". ||
do 2 wp_pure _. by iApply "IH". ||
- wp_alloc l1 as "Hl1". wp_alloc l2 as "Hl2". ||
wp_send with "[$\$$Hl1]". wp_send with "[$\$$Hl2]". ||
wp_recv as "Hl1". wp_recv as "Hl2". ||
wp_load. wp_load. ||
wp_pures. by iApply "HΦ". ||

Proof of message-passing program

The proven lemma is logically equivalent to the specification
$\hoare{\TRUE}{\mathtt{prog\_ref\_swap\_loop}\ ()}{ \Ret \val. \val = 42 }$,
but is presented in weakest precondition style as is common in Iris in Coq.
The initial proof state is:

∀ Φ, Φ$\ $#42 -∗ WP prog_ref_swap_loop #()  v, Φ$\ $v

We start the proof on line:proofsetup by introducing the
postcondition Φ, and the hypothesis
HΦ : Φ$\ $#42,
and then continue by evaluating the lambda expression with wp_lam.
On line:start we apply the specification
start_chan_spec, which is the weakest precondition variant of
Ht-start for
$\startname$ by picking the expected protocol prot_ref_loop.
This leaves us with two subgoals, separated by bullets “-”:
one for the forked-off thread, and one for the main thread.

§.§.§ Proof of the forked-off thread

In the proof of the recursively-defined forked-off thread
we use iLöb as "IH" for Loeb induction on line:forksetup.
This leaves us with the proof state:

"IH" : ▷ (c ↣$\ $iProto_dual prot_ref_loop -∗
WP (rec: "go" "c'" :=
let: "l" := recv "c'" in
"l" <- ! "l" + #2;;
send "c'" #();; "go" "c'") c  _, True )
"Hc" : c ↣$\ $iProto_dual prot_ref_loop
WP (rec: "go" "c'" :=
let: "l" := recv "c'" in
"l" <- ! "l" + #2;;
send "c'" #();; "go" "c'") c  _, True

We now resolve the application of c to the recursive function
with wp_lam.
This lets us strip the later from the Loeb induction hypothesis, as the program
has taken a step.
The proof state is then as follows:

"IH" : c ↣$\ $iProto_dual prot_ref_loop -∗ WP prog_rec c  _, True
"Hc" : c ↣$\ $iProto_dual prot_ref_loop
WP let: "l" := recv c in
"l" <- ! "l" + #2;;
send c #();; prog_rec c  _, True

For brevity's sake we abbreviate the recursive code in "IH" as
prog_rec c.

On line:forkbody we resolve the proof of the body of the recursive function.
So far, the proof only used Iris's standard tactics, we now use the
tactic for receive
wp_recv (l x)$\! $ as "Hl", to resolve the
receive in evaluation position, introducing the received l and x,
along with the predicate of the protocol l ↦$\ $#x naming it
To do so, the protocol is normalised, unfolding the recursive definition once,
as well as resolving the dualisation of the head,
turning it into a receive as expected.
This leads to the following proof state:

"IH" : c ↣$\ $iProto_dual prot_ref_loop -∗ WP prog_rec c  _, True
"Hl" : l ↦$\ $#x
"Hc" : c ↣$\ $iProto_dual (<?> MSG #()  l ↦$\ $#(x + 2) ; prot_ref_loop)
WP let: "l" := #l in
"l" <- ! "l" + #2;;
send c #();; prog_rec c  _, True

We then use the tactics wp_load and wp_store to resolve the
dereferencing and updating of the location:

"IH" : c ↣$\ $iProto_dual prot_ref_loop -∗ WP prog_rec c  _, True
"Hl" : l ↦$\ $#(x + 2)
"Hc" : c ↣$\ $iProto_dual (<?> MSG #()  l ↦$\ $#(x + 2) ; prot_ref_loop)
WP send c #();; prog_rec c   _, True

We then use the tactic wp_send with "[$\$$Hl]" to resolve the
send operation in evaluation
position, by giving up the ownership of "Hl".
Again, the protocol is automatically normalised by resolving the dualisation of the receive
($\RECV$) to obtain the send ($\SEND$) as expected.

We finally close the proof of the forked-off thread on line:forkclose.
We first take two pure evaluation steps revolving the sequencing of operations with
do 2 wp_pure _ to reach the recursive call.
This results in the proof state:

"IH" : c ↣$\ $iProto_dual prot_ref_loop -∗ WP prog_rec c  _, True
"Hc" : c ↣$\ $iProto_dual prot_ref_loop
WP prog_rec c  _, True

We then use by iApply "IH" to close the proof by using the
Loeb induction hypothesis.

§.§.§ Proof of the main thread

The proof of the main thread follows similarly.
On line:mainalloc we use wp_alloc l1 as "Hl1" and
wp_alloc l2 as "Hl2", to resolve the allocations of the new locations,
binding the logical variables of the locations to l1 and l2,
and adding hypotheses "Hl1" and "Hl2" for ownership
of these locations to the separation logic proof context.
The proof state is then:

"HΦ" : Φ$\ $#42
"Hc" : c ↣$\ $prot_ref_loop
"Hl1" : l1 ↦$\ $#18
"Hl2" : l2 ↦$\ $#20
WP send c #l1;; send c #l2;; recv c;; recv c;; ! #l1 + ! #l2  v, Φ$\ $v

On line:mainsend,
we resolve the first send operation with the tactic
wp_send with "[$\$$Hl1]", by giving up
ownership of the location |l1|.
Here, the protocol is normalised by unfolding the recursive definition, after which the
head symbol is a send ($\SEND$) as expected.
The resulting proof state is as follows:

"HΦ" : Φ$\ $#42
"Hl2" : l2 ↦$\ $#20
"Hc" : c ↣$\ $(<?> MSG #()  l1 ↦$\ $#(18 + 2) ; prot_ref_loop)
WP send c #l2;; recv c;; recv c;; ! #l1 + ! #l2  v, Φ$\ $v

To resolve the second send operation, we need to weaken the protocol using swapping
(rule SP-swap'), which is taken care of automatically by the tactic
wp_send with "[$\$$Hl2]".
The normalisation detects that the protocol has a
receive ($\RECV$) as a head symbol, and therefore attempts swapping.
To do so it steps ahead of the receive ($\RECV$), and unfolds the recursive definition,
which results in a send ($\SEND$) as the first symbol after the head.
It then detects that there are no dependencies between the two, and can thus apply
the swapping rule SP-swap', moving the send ($\SEND$) ahead of the
receive ($\RECV$).
With the head symbol now being a send ($\SEND$), the symbolic execution continues as normal,
resulting in the proof state:

"HΦ" : Φ$\ $#42
"Hc" : c ↣$\ $(<?> MSG #()  l1 ↦$\ $#(18 + 2) ;
<?> MSG #()  l2 ↦$\ $#(20 + 2) ; prot_ref_loop)
WP recv c;; recv c;; ! #l1 + ! #l2  v, Φ$\ $v

On line:mainrecv we then proceed as expected with wp_recv as "Hl1"
and wp_recv as "Hl2", to resolve the receive operations, giving us back the updated
point-to resources:

"HΦ" : Φ$\ $#42
"Hl1" : l1 ↦$\ $#(18 + 2)
"Hl2" : l2 ↦$\ $#(20 + 2)
"Hc" : c ↣$\ $prot_ref_loop
WP ! #l1 + ! #l2  v, Φ$\ $v

At line:mainload we then continue by using wp_load twice to
dereference the reacquired and updated locations, and then use trivial symbolic execution
using |wp_pures|
to resolve the remaining computations.
On line:mainclose we finally close the proof by applying the
hypothesis "HΦ" about the postcondition.

§.§ Tactic support for subprotocols

While the tactics automatically apply the subprotocol rules during
symbolic execution, as shown in <Ref>,
we sometimes want to prove subprotocol relations as explicit lemmas.
We have tactic support for such proofs as well.
We extend the existing MoSeL tactics
iIntros, iExists, iFrame, iModIntro,
and iSplitL/iSplitR to automatically use the subprotocol rules to
turn the goal into an equivalent goal where the regular Iris tactics apply.

* iIntros (x1 .. xn)$\! $ "H1 .. Hm"
transforms the subprotocol goal to
begin with n universal quantification and m implications, using the rules
SP-send-elim and SP-recv-elim,
and then introduces the quantifiers (naming them x1 .. xn) into the
Coq context, and the hypotheses (naming them H1 .. Hm) into the
separation logic context.

* iExists (t1 .. tn) transforms the subprotocol goal to start with
n existential quantifiers, using the
SP-send-intro, SP-recv-intro and SP-trans rules,
and then instantiates these quantifiers with the terms t1 .. tn specified by the pattern.

* iFrame "H" transforms the subprotocol goal into a separating
conjunction between the payload predicates of the head symbols of either
protocol, using the rules
SP-send-intro and SP-recv-intro,
and then tries to solve the payload predicate subgoal using |"H"|.

* iModIntro transforms the subprotocol goal into a
goal starting with a later modality ($\later$), using the rules
SP-send-mono and SP-recv-mono,
and then introduces that later by stripping off a later from any hypothesis
in the separation logic context.

* iSplitL/iSplitR "H1 .. Hn" transforms the subprotocol goal into a
separating conjunction between the payload predicates of the head symbols of either
protocol, using the
SP-send-intro, SP-recv-intro and SP-trans rules,
and then creates two subgoals.
For iSplitL the left subgoal is given the hypotheses
H1 .. Hn from the separation logic context,
while the right subgoal is given any remaining hypotheses, and for

The extensions of these tactics are implemented by defining custom type class
instances that hook into the existing MoSeL tactics as described by Krebbers  [55].

Lemma list_rev_subprot :
⊢$\ $(<! (l : loc) (vs : list val)> MSG #l  llist l vs ;
<?> MSG #()  llist internal_eq l (reverse vs) ; END) ⊑
(<! (l : loc) (xs : list T)> MSG #l  llistI IT l xs ;
<?> MSG #()  llistI IT l (reverse xs) ; END).
iIntros (l xs) "Hl". ||
iDestruct (Hlr with "Hl") as (vs) "[Hl HIT]". ||
iExists l, vs. iFrame "Hl". ||
iModIntro.|| iIntros "Hl". ||
iSplitL. ||
rewrite big_sepL2_reverse_2. iApply Hlr. ||
iExists (reverse vs). iFrame "Hl HIT".  ||
done. ||

Proof of subprotocol relation

To demonstrate these tactics, we will go through a proof of the subprotocol relation
for the list reversing service presented in <Ref>:

\[
\begin{array}{@{} l @{} l @{}}
&\sendprot{(\loc:\Loc)(\vec{\val}:\List\ \Val)}{\loc}{\llistref{\loc}{\vec{\val}}}
\recvprot{}{\TT}{\llistref{\loc}{\listrev{\vec{\val}}}}
\protend\\
\subprotop{} &
\sendprot{(\loc:\Loc)(\vec{\var}:\List\ \tvar)}{\loc}
\recvprot{}{\TT}
\protend
\end{array}
\]

Recall that the following conversion between
the list representation predicate with payload $\llistrefI{\interpvar_\tvar}{\loc}{\vec{\var}}$
and one without payload $\llistref{\loc}{\vec{\val}}$ holds:

\[
\texttt{Hlr} \quad : \quad
\textstyle
\llistrefI{\interpvar_\tvar}{\loc}{\vec{\var}} \ \wandIff \
(\Exists \vec{\val}.
\llistref{\loc}{\vec{\val}} \ast
\Sep_{(\var,\val) \in (\vec{\var},\vec{\val})}.
\interpvar_\tvar\ \var\ \val)
\]

The full Coq proof of the subprotocol relation is shown in
The initial proof state is identical to the lemma statement.
On line:sp_send_intro we start by introducing the
l, xs and the payload
llistI IT l xs of the weaker protocol with the tactic
iIntros (l xs)$\! $ "Hl".
This tactic will implicitly apply the rule SP-send-elim, so the goal
starts with a universal quantification
∀ (l : loc) (xs : list T). llistI IT l xs -∗ ...,
which is then introduced based on the regular Iris introduction pattern.
This gives us:

"Hl" : llistI IT l vs
(<! (l : loc) (vs : list val)> MSG #l  llist l vs ;
<?> MSG #()  llist l (reverse vs) ; END) ⊑
(<!> MSG #l; <?> MSG #()  llistI IT l (reverse xs) ; END)

To obtain the payload predicate expected by the stronger protocol,
we use the lemma $\mathtt{Hlr}$,
to derive llist l vs and
[∗ list] x;v ∈$\ $xs;vs, IT x v from
llistI l xs with the tactic
iDestruct (Hlr with "Hl")$\! $ as (vs) "[Hl HIT]" on
The resulting proof state is:

"Hl" : llist l vs
"HIT" : [∗ list] x;v ∈$\ $xs;vs, IT x v
(<! (l : loc) (vs : list val)> MSG #l  llist l vs ;
<?> MSG #()  llist l (reverse vs) ; END) ⊑
(<!> MSG #l; <?> MSG #()  llistI IT l (reverse xs) ; END)

At line:sp_send_elim we
instantiate the of the stronger protocol with the
l and vs using iExists l, vs.
This will implicitly apply the rules SP-send-intro and SP-trans,
which makes the goal
start with ∃ (l : loc)$\! $ (vs : list val), so the existentials
can be instantiated.
To resolve the payload predicate obligation llist l vs, we use
iFrame "Hl".
This uses the rules SP-send-intro and SP-trans to turn the goal into
llist l vs ∗$\ $..., where the left subgoal is resolved using
We then have the following remaining proof state:

"HIT" : [∗ list] x;v ∈$\ $xs;vs, IT x v
(<!> MSG #l; <?> MSG #()  llist l (reverse vs) ; END) ⊑
(<!> MSG #l; <?> MSG #()  llistI IT l (reverse xs) ; END)

As the head symbols of both protocols are sends ($\SEND$) with no or
payload predicates, we use iModIntro
on line:sp_send_mono, which first applies
SP-send-mono to step over the sends, and then
introduces the later modality ($\later$).
This gives us the proof state:

"HIT" : [∗ list] x;v ∈$\ $xs;vs, IT x v
(<?> MSG #()  llist l (reverse vs) ; END) ⊑
(<?> MSG #()  llistI IT l (reverse xs) ; END)

On line:sp_recv_intro, similarly to before, we use
iIntros "Hl", to introduce the payload predicate,
but this time we do it for the stronger protocol,
as dictated by SP-recv-elim:

"HIT" : [∗ list] x;v ∈$\ $xs;vs, IT x v
"Hl" : llist l (reverse vs)
(<?> MSG #() ; END) ⊑
(<?> MSG #()  llistI IT l (reverse xs) ; END)

To resolve the payload predicate of the weaker protocol, we use
iSplitL "Hl HIT" on line:sp_recv_elim, that first use
SP-recv-intro and SP-trans, to turn the goal into
llistI IT l (reverse xs)$\ $∗$\ $..., and then use the goal splitting pattern
of Iris, to give us two subgoals, where we use the hypotheses "Hl" and
"HIT" in the left subgoal.
The first subgoal is then:

"HIT" : [∗ list] x;v ∈$\ $xs;vs, IT x v
"Hl" : llist l (reverse vs)
llistI IT l (reverse xs)

On line:sp_sg_11, we first use the lemma Hlr
in the right-to-left
direction, and then rewrite the hypothesis "HIT" using a
lemma from the Iris library with rewrite big_sepL2_reverse_2.
We do this to obtain [∗ list] x;v ∈$\ $reverse xs;reverse vs, IT x v,
in order to match the proof goal.
This gives the proof obligation:

"HIT" : [∗ list] x;v ∈$\ $reverse xs;reverse vs, IT x v
"Hl" : llist l (reverse vs)
∃$\ $vs : list val, llist l vs ∗$\ $([∗ list] x;v ∈ reverse xs;vs, IT x v)

We finally close the proof on line:sp_sg_12
with iExists (reverse vs), followed by
iFrame "Hl HIT", as the goal matches the hypotheses exactly,
when picking reverse vs as the existential quantification.
We then move on to the second subgoal:

(<?> MSG #(); END) ⊑$\ $(<?> MSG #(); END)

We resolve this subgoal, on line:sp_sg_2,
with the tactic done,
which tries to close the proof, by automatically applying

§ RELATED WORK

This section elaborates on the relation to
message passing in separation logic (<Ref>) and
process calculi (<Ref>),
session types (<Ref>),
session subtyping (<Ref>),
endpoint sharing (<Ref>),
and verification of map-reduce (<Ref>).

§.§ Message passing and separation logic

Lozes and Villard [84, 59] present a logic for contract-based
reasoning about programs in a small imperative language with
bi-directional asynchronous channels.
Contracts are represented by finite-state automata with labelled send or receive
transitions, equipped with separation logic predicates.
Similar to session types (and ), contracts have a notion of duality, but
unlike they do not support dependencies between messages.
Their logic
supports ownership transfer (including ownership transfer of channels, akin to
delegation), session-type like choice, and a form of recursive contracts.
Their language has a close operation for channel deallocation
instead of being garbage collected.
A restriction to structured concurrency
(par instead of fork-based), structured channel deallocation (must close both
endpoints together) and linear (instead of affine) logic ensures memory-leak freedom.
A form of channel sharing is supported, which we further discuss in <Ref>.

Craciun  [17] introduced session logic, a variant of
separation logic that includes
predicates for protocol specifications similar to ours.
This work includes support for mutable state,
ownership transfer (including ownership transfer of channels, akin to delegation),
session-type like choice using a special type of disjunction operator on
the protocol level, and a sketch of an approach to verify deadlock
freedom of programs.
Combined, these features allow them to verify
interesting and non-trivial
message-passing programs.
Their logic as a whole is not
higher-order, which means that sending functions over channels is not
Moreover, their logic does not support protocol-level that can connect the
transferred message with the tail protocol.
It is therefore not possible to model dependent protocols like we do in .
Their work includes a notion of subtyping as weakening and strengthening of the
payload predicates, however they do not consider swapping, and do not allow
manipulation of resources as a part of their subtyping relation.
There also exists
no support for other concurrency primitives such as locks, which by
extension means that manifest sharing is not possible.
In we get this for free by building on top of Iris, and reusing its ghost state mechanism.
Their work has not been
mechanised in a proof assistant, but example programs can
be checked using the HIP/SLEEK verifier.

The original Iris paper [50] includes a small
message-passing language with
channels that do not preserve message order.
It was included to demonstrate that Iris is flexible enough to handle other
concurrency models than standard shared-memory concurrency.
Since the Hoare triples for send and receive reason about
the entire channel buffer, protocol reasoning
must be done via STSs or other forms of ghost state.

Hamin and Jacobs [38] take an orthogonal direction and use separation
logic to prove deadlock freedom of programs that communicate via
message passing using a custom logic tailored to this purpose.
They do not provide abstractions akin to our session-type based protocols.
Instead one has to reason using invariants and ghost state explicitly.

Mansky  [60] verify the functional
correctness of a message-passing system written in C using the VST framework
in Coq [5].
While they do not verify message-passing programs
like we do, they do verify that the implementation of their message-passing
system is resilient to faulty behaviour in the presence of malicious senders
and receivers.

Tassarotti  [79] prove correctness
and termination preservation of a compiler from a simple language with session
types to a functional language with mutable state, where channels are
implemented using references on the heap.
This work is also done in Iris in Coq.
The session types they consider are more like standard session types, which
cannot express functional properties of messages, but only their types.

The Disel logic by Sergey  [75] and the Aneris logic
by Krogh-Jespersen  [56] can be used to reason about message-passing programs
that work on network sockets.
Channels can only be used to send strings, are not order preserving, and
messages can be dropped but not duplicated.
Since only strings are sent over channels complex data (such as functions) must
be marshalled and unmarshalled in order to be sent over the network.
Both Disel and Aneris therefore address a different problem than we do.

SteelCore [73] is a framework for
concurrent separation logic embedded in the F$\star$ language.
SteelCore has been used to encode unidirectional synchronous channels that
can be typed with protocols akin to session types.
Their protocols are defined as a dependent sequence of value obligations with
associated separation logic predicates, dictating what can be sent over the channel,
including the transfer of ownership.
Channels are first-class and can also be transferred (akin to delegation),
but their protocols do not include higher-order protocol-level ,
or subtyping.
They postulated that their approach scales to bidirectional asynchronous
communication, but left that for future work.

§.§ Separation logic and process calculi

Another approach to verify message-passing programs is to combine
separation logic and process calculus.
Neither of the approaches below support delegation or concurrency paradigms
other than message passing.

Francalanza  [28] use separation logic to verify
programs written in a CCS-like language.
Channels model memory location, which has the effect that their input-actions
behave a lot like our updates of mutable state with variable
substitutions updating the state. As a proof of concept they prove the
correctness of an in-place quick-sort algorithm.

Oortwijn  [67] use separation logic and the mCRL2 process
calculus to model communication protocols.
The logic itself operates on a high level of abstraction and deals exclusively
with intraprocess communication where a fractional separation logic is
used to distribute channel resources to concurrent threads.
Protocols are extracted from code, but there is no formal connection
between the specification logic and the underlying language.

§.§ Session types

Seminal work on linear type systems for the $\pi$-calculus by
Kobayashi  [54] led to the creation of binary session types
by Honda  [41], and consequentially multiparty session types
by Honda  [42].

Later work by Dardha  [23] helped merge the linear type
systems of Kobayashi with Honda's session types, which facilitated the
incorporation of session types in mainstream programming
languages like Go [58],
OCaml [70, 44], and
Java [39].
These works focus on adding session-typed support for
message passing in existing languages, but do not
target functional correctness.

Bocchi  [11] pushed the boundaries of
what can be verified with (multiparty) session types while staying within a
decidable fragment of first-order logic.
They use first-order predicates to describe
properties of values being sent and received.
Decidability is maintained by imposing restrictions on these predicates, such
as ensuring that nothing is sent that will be invalidated down the line.
The constraints on the logic do, however, limit what programs can be
The work includes standard subtyping on communicated values and on choices,
but no notion of swapping sends ahead of receives.

Caires and Pfenning [20] discovered a correspondence between intuitionistic
linear logic and $\pi$-calculus with session types, which was extended with
quantifiers and dependent types by Toninho  [76].
These quantifiers range over both terms and propositions of an LF-based
logic [19], and can be used to specify basic properties of
the exchanged values.
Toninho and Yoshida [82] extended this work by allowing the
structure of the protocol to depend on the quantifiers.
This notion of dependency allows for protocols where the length of the (tail)
protocol depends on the values that were previously exchanged, similar to what
we do in <Ref>.
Finally, Das and Pfenning [24, 25] developed a
dependent session-type system with domain-specific logic for verifying
arithmetic properties of programs with message passing.

Another approach to dependent session types was carried out by
Thiemann and Vasconcelos [81] who introduced label-dependent
session types.
They unify universal and existential quantifiers with the
send and receive primitives of conventional session types.
Hence, similar to , the choice connectives ($\branchop$ and $\selectop$)
can be derived.

Toninho  [77] and Lindley and
Morris [57] developed session-type systems with
termination guarantees in the presence of recursive (session) types.
This is achieved by imposing a discipline similar to (co)inductive definitions
in Coq and Agda.
In contrast, poses no usage discipline on recursive ,
and hence guarantees partial correctness.

§.§ Session subtyping

's subprotocol relation is inspired by the notion of session subtyping,
for which seminal work was carried out by Gay and Hole [31].
Mostrous  [64] extended session subtyping to
multiparty asynchronous session types, and as part of that, introduced the notion of
swapping sends ahead of receives for independent channels.
Mostrous  [63] later considered swapping over the same channel in
the context of binary session types.
Our subprotocol relation is most closely related to the work of
Mostrous  [63],
although they define subtyping as a simulation on infinite trees,
using so-called asynchronous contexts, whereas we define it using Iris's
support for guarded recursion.
It should be noted that the work by Gay and Hole [31] differs
from the work by Mostrous  [64] and
Mostrous  [63] in the orientation of the subtyping relation,
as discussed by Gay [29].
Our subprotocol relation uses the orientation of
Gay and Hole [31].

Session subtyping for recursive type systems is universally carried out as a type
simulation on infinite trees
[31, 64, 63],
which complicates subtyping under the recursion operator.
Bernardi  [8] and Gay  [33] provide further insights on
this problem, although they primarily investigate duality rather than subtyping.

To reason about recursive subtyping, Brand and Henglein [10] present
a coinductive formulation of subtyping
(which they apply to regular type systems, rather than session types).
We use a similar coinductive formulation, but instead of ordinary coinduction,
we use Iris's support for guarded recursion, which lets us
prove subtyping relations of recursive protocols using Loeb induction.

§.§ Endpoint sharing

One of the key features of conventional session types is that endpoints are owned
by a single thread.
While endpoints can be delegated (transferred from one thread to
another), they typically cannot be shared (be accessed by multiple threads
However, as demonstrated in <Ref>, sharing channels
endpoints is often desirable, and possible in .

As a simple way to relax this limitation of sharing in conventional
session types,
Vasconcelos [83] allows session types of the form
$(\MU \recname. \sendtype{\tvar}{\recname})$ or
$(\MU \recname. \recvtype{\tvar}{\recname})$ to be shared.
Lozes and Villard [59] present a similar idea in the context of their
contract-based separation logic (see also <Ref>) by equipping
the connective for channel endpoint ownership with a fractional permission.
If the fraction is smaller than 1, then the endpoint can be shared, but at the
cost of only permitting transitions to the same contract state.
Using fractional permissions they prove a lock specification à la
Gotsman  [30] of an implementation of locks in terms of channels.
This approach to locks is dual to ours in , where we implement
channels in terms of locks.
Unlike Iris (and ), their logic does not support ghost state, so
it cannot express complex protocols like the ones from <Ref>.

In the $\pi$-calculus community there has been prior work
on endpoint sharing, by
Atkey  [2], Kobayashi [53], and
Padovani [69].
The latest contribution in this line of work is by
Balzer  [15], who
developed a type system based on session types with
support for manifest sharing.
Manifest sharing is the notion of sharing a channel endpoint
between multiple processes using a lock-like structure to ensure mutual
Their key idea to ensure mutual exclusion using a type system is to use
adjoint modalities to connect two classes of types: types
that are linear, and thus denote unique channel ownership, and types that are
unrestricted, and thus can be shared.
The approach to endpoint sharing in is different:
do not include a built-in notion for endpoint sharing, but can be combined
with Iris's general-purpose mechanisms for sharing, like locks.

§.§ Verification of map-reduce

To our knowledge the only verification related to the map-reduce model
[22] is by
Ono  [68], who made two mechanisations in Coq. The first took
a functional model of map-reduce and verified a few specific mappers
and reducers, extracted these to Haskell, and ran them using Hadoop
Streaming. The second did the same by annotating Java mappers and
reducers using JML
and proving them correct using the Krakatoa tool [62], using
a combination of
SAT-solvers and the Coq proof assistant. While they worked on
verifying specific mappers and reducers, our case study focuses on
verifying the communication of a map-reduce model that can later be parameterised with
concrete mappers and reducers.

§ CONCLUSION AND FUTURE WORK

In this paper, we have given a comprehensive account of the concurrent
separation logic for proving functional correctness of programs that
combine message-passing with other programming and concurrency paradigms.
The core feature of its its mechanism of , which is inspired by session types.
Considering the rich literature on session types and concurrent separation
logic, we expect there to be many promising directions for future work.

§.§.§ Multi-party

The formalism of multi-party session types [42]
applies to message-passing communication between more
than two parties (threads or processes).
The key ingredient of multi-party session types is the notion of a
global protocol, which specifies the permitted communication for
multiple parties of a system.
From the global protocol one can then generate local protocols for the
individual parties.
It would be interesting to explore a multi-party version of .
Prior work by Costea  [16] on multi-party session logic and
Zhoud  [85] on refined multiparty session types could serve
as a starting point.

§.§.§ Deadlock freedom

As discussed in <Ref>, deadlocks are valid behaviours
according to the notion of safety used in Iris (and thus ).
Many conventional session type systems do not consider deadlocks to be valid
behaviours, but achieve that at the
expense of prohibiting valid (deadlock free) programs that can be verified
in .

A direction for future work is to develop a variant of that incorporates
the usual restrictions of session-type systems like
linearity and a $\startname$ primitive for combined channel and thread creation.
To prove an adequacy theorem that ensures that this variant of indeed
prohibits deadlocks, one needs to change the
model of to ensure acyclicity of the dependency structure among the threads
and channels.
This could be achieved by building upon recent work
by Bizjak  [9] on linearity in Iris and by Jacobs  [45]
on a separation-logic based proof method for deadlock freedom of session types.
Additionally, one could consider a version
of without garbage collection but with a $\derivedkw{close}$
instruction for channel
deallocation, and prove that it indeed guarantees memory-leak freedom.

Another direction for future work is to develop a separation logic
that combines session-type based deadlock freedom with lock-order based
deadlock freedom to prove deadlock freedom of programs that combine
message passing with other concurrency mechanisms like locks.
The work by Hamin and Jacobs [38] on reasoning about lock orders in separation
logic, and the work by Balzer  [15] on deadlock freedom for manifest
sharing might provide valuable insights, but figuring out how to combine these
two approaches with
Iris and is a challenging open problem.

§ ACKNOWLEDGMENTS

We thank the anonymous reviewers of both this paper and the
POPL'20 conference version for their helpful feedback.
We are grateful to Andreea Costea, Daniel Gratzer, Daniël Louwrink, Fabrizio Montesi,
Marco Carbone,
and the participants of the Iris workshop 2019 for discussions.
The third author (Robbert Krebbers) was supported by the Dutch Research Council (NWO), project 016.Veni.192.259.

[1]
Amal Ahmed.
Semantics of Types for Mutable State.
PhD thesis, Princeton University, 2004.

[2]
Robert Atkey, Sam Lindley, and J. Garrett Morris.
Conflation confers concurrency.
In Essays Dedicated to Philip Wadler on the Occasion of His 60th
Birthday, pages 32–55, 2016.

[3]
Andrew W. Appel and David McAllester.
An indexed model of recursive types for foundational proof-carrying
TOPLAS, 23(5):657–683, 2001.

[4]
Andrew W. Appel, Paul-André Melliès, Christopher D. Richards, and
Jérôme Vouillon.
A very modal model of a modern, major, general type system.
In POPL, pages 109–122, 2007.

[5]
Andrew W. Appel.
Program Logics for Certified Compilers.
Cambridge University Press, 2014.

[6]
Pierre America and Jan J. M. M. Rutten.
Solving reflexive domain equations in a category of complete metric
JCSS, 39(3):343–375, 1989.

[7]
Lars Birkedal and Aleš Bizjak.
Lecture notes on iris: Higher-order concurrent separation logic.
<https://iris-project.org/tutorial-material.html>, 2020.

[8]
Giovanni Bernardi, Ornela Dardha, Simon J. Gay, and Dimitrios Kouzapas.
On duality relations for session types.
In TGC, volume 8902 of LNCS, pages 51–66, 2014.

[9]
Ales Bizjak, Daniel Gratzer, Robbert Krebbers, and Lars Birkedal.
Iron: Managing obligations in higher-order concurrent separation
PACMPL, 3(POPL):65:1–65:30, 2019.

[10]
Michael Brandt and Fritz Henglein.
Coinductive axiomatization of recursive type equality and subtyping.
Fundamenta Informaticae, 33(4):309–338, 1998.

[11]
Laura Bocchi, Kohei Honda, Emilio Tuosto, and Nobuko Yoshida.
A theory of design-by-contract for distributed multiparty
In CONCUR, pages 162–176, 2010.

[12]
Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, and Kristian
First steps in synthetic guarded domain theory: Step-indexing in the
topos of trees.
LMCS, 8(4), 2012.

[13]
Stephanie Balzer and Frank Pfenning.
Manifest sharing with session types.
PACMPL, 1(ICFP):37:1–37:29, 2017.

[14]
Lars Birkedal, Kristian Støvring, and Jacob Thamsborg.
The category-theoretic solution of recursive metric-space equations.
TCS, 411(47):4102–4122, 2010.

[15]
Stephanie Balzer, Bernardo Toninho, and Frank Pfenning.
Manifest Deadlock-Freedom for Shared Session Types.
In ESOP, pages 611–639, 2019.

[16]
Andreea Costea, Wei-Ngan Chin, Shengchao Qin, and Florin Craciun.
Automated modular verification for relaxed communication protocols.
In APLAS, pages 284–305, 2018.

[17]
Florin Craciun, Tibor Kiss, and Andreea Costea.
Towards a session logic for communication protocols.
In ICECCS, pages 140–149, 2015.

[18]
Coq Development Team.
The Coq proof assistant reference manual, version 8.12.0.
URL: <https://coq.inria.fr/distrib/current/refman/>.

[19]
Iliano Cervesato and Frank Pfenning.
A linear logical framework.
In LICS, pages 264–275, 1996.

[20]
Luís Caires and Frank Pfenning.
Session types as intuitionistic linear propositions.
In CONCUR, pages 222–236, 2010.

[21]
Derek Dreyer, Amal Ahmed, and Lars Birkedal.
Logical step-indexed logical relations.
LMCS, 7(2), 2011.

[22]
Jeffrey Dean and Sanjay Ghemawat.
Mapreduce: Simplified data processing on large clusters.
In OSDI, pages 137–150, 2004.

[23]
Ornela Dardha, Elena Giachino, and Davide Sangiorgi.
Session types revisited.
In PPDP, pages 139–150, 2012.

[24]
Ankush Das and Frank Pfenning.
Session types with arithmetic refinements.
In CONCUR, volume 171 of LIPIcs, pages 13:1–13:18, 2020.

[25]
Ankush Das and Frank Pfenning.
Verified linear session-typed concurrent programming.
In PPDP, pages 7:1–7:15. ACM, 2020.

[26]
Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner.
Tada: A logic for time and data abstraction.
In ECOOP, pages 207–231, 2014.

[27]
Matthias Felleisen and Robert Hieb.
The revised report on the syntactic theories of sequential control
and state.
TCS, 103(2):235–271, 1992.

[28]
Adrian Francalanza, Julian Rathke, and Vladimiro Sassone.
Permission-based separation logic for message-passing concurrency.
LMCS, 7(3), 2011.

[29]
Simon J. Gay.
Subtyping supports safe session substitution.
In A List of Successes That Can Change the World - Essays
Dedicated to Philip Wadler on the Occasion of His 60th Birthday, pages
95–108, 2016.

[30]
Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, and Mooly Sagiv.
Local reasoning for storable locks and threads.
In Zhong Shao, editor, APLAS, volume 4807 of LNCS, pages
19–37, 2007.

[31]
Simon J. Gay and Malcolm Hole.
Subtyping for session types in the pi calculus.
Acta Informatica, 42(2-3):191–225, 2005.

[32]
Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, and
Robbert Krebbers.
Scala step-by-step: Soundness for DOT with step-indexed logical
relations in Iris.
PACMPL, 4(ICFP):114:1–114:29, 2020.

[33]
Simon J. Gay, Peter Thiemann, and Vasco T. Vasconcelos.
Duality of session types: The final cut.
In PLACES, volume 314 of EPTCS, pages 23–33, 2020.

[34]
Aquinas Hobor, Andrew Appel, and Francesco Nardelli.
Oracle semantics for concurrent separation logic.
In ESOP, volume 4960 of LNCS, pages 353–367. 2008.

[35]
Jonas Kastberg Hinrichsen, Jesper Bengtson, and Robbert Krebbers.
Actris: Session-type based reasoning in separation logic.
PACMPL, 4(POPL):6:1–6:30, 2020.

[36]
Jonas Kastberg Hinrichsen, Jesper Bengtson, and Robbert Krebbers.
Coq mechanisation of actris, 2021.
Available online at

[37]
Carl Hewitt, Peter Bishop, and Richard Steiger.
A Universal Modular ACTOR Formalism for Artificial Intelligence.
In IJCAI, pages 235–245, 1973.

[38]
Jafar Hamin and Bart Jacobs.
Transferring obligations through synchronizations.
In ECOOP, pages 19:1–19:58, 2019.

[39]
Raymond Hu, Dimitrios Kouzapas, Olivier Pernet, Nobuko Yoshida, and Kohei
Type-safe eventful sessions in java.
In ECOOP, pages 21–25, 2010.

[40]
Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, and Jesper
Machine-checked semantic session typing.
In CPP, pages 178–198, 2021.

[41]
Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo.
Language primitives and type discipline for structured
communication-based programming.
In ESOP, pages 122–138, 1998.

[42]
Kohei Honda, Nobuko Yoshida, and Marco Carbone.
Multiparty asynchronous session types.
In POPL, pages 273–284, 2008.

[43]
Iris Development Team.
The mechanisation of Iris.
URL: <https://gitlab.mpi-sws.org/iris/iris/>.

[44]
Keigo Imai, Nobuko Yoshida, and Shoji Yuen.
Session-ocaml: A session-based library with polarities and lenses.
Science of Computer Programming, 172:135–159, 2019.

[45]
Jules Jacobs, Stephanie Balzer, and Robbert Krebbers.
Connectivity graphs: A method for proving deadlock freedom based on
separation logic, 2021.
Manuscript under submission.

[46]
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer.
Rustbelt: Securing the foundations of the rust programming language.
PACMPL, 2(POPL):66:1–66:34, 2018.

[47]
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer.
Safe systems programming in rust.
CACM, 64(4):144–152, 2021.

[48]
Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer.
Higher-order ghost state.
In ICFP, pages 256–269, 2016.

[49]
Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars
Birkedal, and Derek Dreyer.
Iris from the ground up: A modular foundation for higher-order
concurrent separation logic.
JFP, 28:e20, 2018.

[50]
Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars
Birkedal, and Derek Dreyer.
Iris: Monoids and invariants as an orthogonal basis for concurrent
In POPL, pages 637–650, 2015.

[51]
Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek
Dreyer, and Lars Birkedal.
The essence of higher-order concurrent separation logic.
In ESOP, pages 696–723, 2017.

[52]
Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti,
Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, and Derek Dreyer.
Mosel: A general, extensible modal framework for interactive proofs
in separation logic.
PACMPL, 2(ICFP):77:1–77:30, 2018.

[53]
Naoki Kobayashi.
A new type system for deadlock-free processes.
In CONCUR, pages 233–247, 2006.

[54]
Naoki Kobayashi, Benjamin C. Pierce, and David N. Turner.
Linearity and the pi-calculus.
In POPL, pages 358–371, 1996.

[55]
Robbert Krebbers, Amin Timany, and Lars Birkedal.
Interactive proofs in higher-order concurrent separation logic.
In POPL, pages 205–217, 2017.

[56]
Morten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Simon Oddershede
Gregersen, and Lars Birkedal.
Aneris: A mechanised logic for modular reasoning about distributed
In ESOP, pages 336–365, 2020.

[57]
Sam Lindley and J. Garrett Morris.
Talking bananas: Structural recursion for session types.
In ICFP, pages 434–447, 2016.

[58]
Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida.
A static verification framework for message passing in go using
behavioural types.
ICSE, pages 1137–1148, 2018.

[59]
Étienne Lozes and Jules Villard.
Shared contract-obedient endpoints.
In ICE, pages 17–31, 2012.

[60]
William Mansky, Andrew W. Appel, and Aleksey Nogin.
A verified messaging system.
PACMPL, 1(OOPSLA):87:1–87:28, 2017.

[61]
Yusuke Matsushita and Jacques-Henri Jourdan.
Flexible number of logical steps per physical step, 2020.
Iris merge request.
URL: <https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/595>.

[62]
Claude Marché, Christine Paulin-Mohring, and Xavier Urbain.
The KRAKATOA tool for certification of JAVA/JAVACARD programs
annotated in JML.
JLP, (1-2):89–106, 2004.

[63]
Dimitris Mostrous and Nobuko Yoshida.
Session typing and asynchronous subtyping for the higher-order
\(\pi\)-calculus.
Information and Computation, 241:227–263, 2015.

[64]
Dimitris Mostrous, Nobuko Yoshida, and Kohei Honda.
Global principal typing in partially commutative asynchronous
In ESOP, pages 316–332, 2009.

[65]
Hiroshi Nakano.
A modality for recursion.
In LICS, pages 255–266, 2000.

[66]
Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, and Germán Andrés
Communicating state transition systems for fine-grained concurrent
In ESOP, pages 290–310, 2014.

[67]
Wytse Oortwijn, Stefan Blom, and Marieke Huisman.
Future-based static analysis of message passing programs.
In PLACES, pages 65–72, 2016.

[68]
Kosuke Ono, Yoichi Hirai, Yoshinori Tanabe, Natsuko Noda, and Masami Hagiya.
Using coq in specification and program extraction of hadoop mapreduce
In SEFM, pages 350–365, 2011.

[69]
Luca Padovani.
Deadlock and lock freedom in the linear $\pi$-calculus.
In CSL, pages 72:1–72:10, 2014.

[70]
Luca Padovani.
A simple library implementation of binary sessions.
JFP, 27(2010):e4, 2017.

[71]
Kasper Svendsen and Lars Birkedal.
Impredicative concurrent abstract predicates.
In ESOP, pages 149–168, 2014.

[72]
Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert
Krebbers, Derek Dreyer, and Lars Birkedal.
Transfinite Iris: Resolving an existential dilemma of step-indexed
separation logic.
In PLDI, pages 80–95, 2021.

[73]
Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, and
Guido Martínez.
SteelCore: An extensible concurrent separation logic for effectful
dependently typed programs.
PACMPL, 4(ICFP):121:1–121:30, 2020.

[74]
Kasper Svendsen, Filip Sieczkowski, and Lars Birkedal.
Transfinite step-indexing: Decoupling concrete and logical steps.
In ESOP, pages 727–751, 2016.

[75]
Ilya Sergey, James R. Wilcox, and Zachary Tatlock.
Programming and proving with distributed protocols.
PACMPL, 2(POPL):28:1–28:30, 2018.

[76]
Bernardo Toninho, Luís Caires, and Frank Pfenning.
Dependent session types via intuitionistic linear type theory.
In PPDP, pages 161–172, 2011.

[77]
Bernardo Toninho, Luís Caires, and Frank Pfenning.
Corecursion and non-divergence in session-typed processes.
In TGC, volume 8902 of LNCS, pages 159–175, 2014.

[78]
Samira Tasharofi, Peter Dinges, and Ralph E. Johnson.
Why do scala developers mix the actor model with other concurrency
In ECOOP, pages 302–326, 2013.

[79]
Joseph Tassarotti, Ralf Jung, and Robert Harper.
A higher-order logic for concurrent termination-preserving
In ESOP, pages 909–936, 2017.

[80]
Tengfei Tu, Xiaoyu Liu, Linhai Song, and Yiying Zhang.
Understanding real-world concurrency bugs in go.
In ASPLOS, pages 865–878, 2019.

[81]
Peter Thiemann and Vasco T. Vasconcelos.
Label-dependent session types.
PACMPL, 4(POPL):67:1–67:29, 2020.

[82]
Bernardo Toninho and Nobuko Yoshida.
Depending on session-typed processes.
In FOSSACS, volume 10803 of LNCS, pages 128–145, 2018.

[83]
Vasco Thudichum Vasconcelos.
Fundamentals of session types.
Information and Computation, 217:52–70, 2012.

[84]
Jules Villard, Étienne Lozes, and Cristiano Calcagno.
Proving copyless message passing.
In APLAS, pages 194–209, 2009.

[85]
Fangyi Zhou, Francisco Ferreira, Raymond Hu, Rumyana Neykova, and Nobuko
Statically verified refinements for multiparty protocols.
PACMPL, 4(OOPSLA), 2020.