elimination may proceed by removing topmost cuts. In there is no
such notion as a topmost cut since proofs may be infinite. As a
consequence, the cut elimination result for is proved by eliminating
bottom-most cuts [Baelde et al., 2022]. This strategy fits perfectly with
the reduction semantics of  – and that of any other conventional
process calculus, for that matter – whereby reduction rules act only on the
exposed (unguarded) part of processes but not behind prefixes. As a result,
the reduction semantics of is completely ordinary, unlike other
logically-inspired process calculi that incorporate commuting conversions
[Wadler, 2014, Lindley and Morris, 2016], perform reductions behind
prefixes [Qian et al., 2021] or swap prefixes [Bellin and Scott, 1994].

In <Ref> we have proposed a type system
ensuring the fair termination of binary/multiparty sessions.
In the present chapter we achieve the
same objective using a more basic process calculus and exploiting its strong
logical connection with . In fact, the soundness proof of our type system
piggybacks on the cut elimination property of .
Other session typed calculi based on linear logic with fixed points have been
studied by [Lindley and Morris, 2016] and [Derakhshan and Pfenning, 2019, Derakhshan, 2021].

The type systems described in these works respectively guarantee termination and
strong progress, whereas our type system guarantees fair termination which is
somewhat in between these properties. Overall, our type system seems to hit a
sweet spot: on the one hand, it is deeply rooted in linear logic and yet it can
deal with common communication patterns (like the buyer/seller interaction
described above) that admit potentially infinite executions and therefore are
out of scope of other logic-inspired type systems; on the other hand, it
guarantees lock freedom [Kobayashi, 2002, Padovani, 2014], strong
progress <cit.> and also termination, under a
suitable fairness assumption.

The chapter is organized as follows.
In <Ref> we show the definition of the types bu relying on
the formulas of linear logic. Notably, these contain least/greatest fixed points.
In <Ref> we present syntax and semantics of .
<Ref> introduces the type system for as well as the
validity conditions.
As usual, we dedicate <Ref> to detail the soundness proof
of the type system and <Ref> to discuss about related works.
Finally, we are now able to make a comparison between the present type system and
those presented in <Ref>.
We make such comparison by examples in <Ref>.

§ TYPES AND FORMULAS

The types of are built using the multiplicative additive fragment of
linear logic enriched with least and greatest fixed points. In this section we
specify the syntax of types along with all the auxiliary notions that are needed
to present the type system and prove its soundness.

The syntax of pre-formulas relies on an infinite set of propositional
variables ranged over by $X$ and $Y$ and is defined by the grammar below:

\[
\begin{array}{rcl}
\FormulaF, \FormulaG &
::= &
\Zero \mid
\Top \mid
\One \mid
\Bot \mid
\FormulaF \plinchoice \FormulaG \mid
\FormulaF \plinbranch \FormulaG \mid
\FormulaF \tfork \FormulaG \mid
\FormulaF \tjoin \FormulaG \mid
\tmu\X.\Formula \mid
\tnu\X.\Formula \mid
\end{array}
\]

As usual, $\tmu$ and $\tnu$ are the binders of propositional variables and the
notions of free and bound variables are defined accordingly. We assume that the
body of fixed points extends as much as possible to the right of a pre-formula,
so $\tmu\X.X \plinchoice \One$ means $\tmu\X.(X \plinchoice \One)$ and not $(\tmu\X.X)
\plinchoice \One$. We write $\subst\Formula\X$ for the capture-avoiding substitution
of all free occurrences of $X$ with $\Formula$.

We write $\dual\Formula$ for the
dual of $\Formula$, which is the involution defined by the equations

\[
\begin{array}{*{6}{@{}r@{~}c@{~}l@{\quad}}@{}}
\dual\Zero & = & \Top & \qquad
\dual{(\FormulaF \plinchoice \FormulaG)} & = & \dual\FormulaF \plinbranch \dual\FormulaG & \qquad
\dual{(\tmu\X.\Formula)} & = & \tnu\X.\dual\Formula &
\\
\dual\One & = & \Bot &
\dual{(\FormulaF \tfork \FormulaG)} & = & \dual\FormulaF \tjoin \dual\FormulaG &
\dual\X & = & X
\end{array}
\]

A formula is a closed pre-formula.

In the context of , formulas
describe how linear channels are used. Positive formulas (those built with the
constants $\Zero$ and $\One$, the connectives $\plinchoice$ and $\tfork$ and the
least fixed point) indicate output operations whereas negative formulas (the
remaining forms) indicate input operations. The formulas $\FormulaF \plinchoice
\FormulaG$ and $\FormulaF \plinbranch \FormulaG$ describe a linear channel used for
sending/receiving a tagged channel of type $\FormulaF$ or $\FormulaG$. The tag
(either $\LeftTag$ or $\RightTag$) distinguishes between the two possibilities.
The formulas $\FormulaF \tfork \FormulaG$ and $\FormulaF \tjoin \FormulaG$
describe a linear channel used for sending/receiving a pair of channels of type
$\FormulaF$ and $\FormulaG$; $\tmu\X.\Formula$ and $\tnu\X.\Formula$ describe a
linear channel used for sending/receiving a channel of type
$\Formula\subst{\tmu\X.\Formula}\X$ or $\Formula\subst{\tnu\X.\Formula}\X$
respectively. The constants $\One$ and $\Bot$ describe a linear channel used for
sending/receiving the unit. Finally, the constants $\Zero$ and $\Top$
respectively describe channels on which nothing can be sent and from which
nothing can be received.

Looking at the structure of buyer and seller in
<Ref>, we can make an educated guess on the type of the
channel they use. Indeed, we see that it is used according to
$\FormulaF \eqdef \tmu\X.X \plinchoice \One$ by buyer and according to
$\FormulaG \eqdef \tnu\X.X \plinbranch \Bot$ in seller.
Note that $\FormulaF = \dual\FormulaG$,
suggesting that seller and seller may interact correctly when connected.

We write $\subf$ for the subformula ordering, that is the least partial
order such that $\FormulaF \subf \FormulaG$ if $\FormulaF$ is a subformula of

For example, consider $\FormulaF \eqdef \tmu\X.\tnu\Y.X \plinchoice Y$
and $\FormulaG \eqdef \tnu\Y.\FormulaF \plinchoice Y$. Then we have $\FormulaF \subf
\FormulaG$ and $\FormulaG \not\subf \FormulaF$. When $\Formulas$ is a set of
formulas, we write $\minf\Formulas$ for its $\subf$-minimum formula if it
is defined.

Occasionally we let $\star$ stand for an arbitrary binary connective $\plinchoice$,
$\tfork$, $\plinbranch$, or $\tjoin$ and $\sigma$ stand for an arbitrary fixed point
operator $\tmu$ or $\tnu$.

When two processes interact on some channel $x$, they may exchange other
channels on which their interaction continues. We can think of these subsequent
interactions stemming from a shared channel $x$ as being part of the same
conversation (the literature on sessions [Honda, 1993, Hüttel et al., 2016]
builds on this idea [Kobayashi, 2002, Dardha et al., 2017]). The
soundness proof of the type system is heavily based on the proof of the cut
elimination property of , which relies on the ability to uniquely
identify the types of the channels that belong to the same conversation and to
trace conversations within typing derivations. Following the literature on
[Baelde et al., 2016, Doumane, 2017, Baelde et al., 2022], we annotate
formulas with addresses.

We assume an infinite set $\AddressSet$ of atomic addresses,
$\dual\AddressSet$ being the set of their duals such that $\AddressSet \cap
\dual\AddressSet = \emptyset$ and $\dual{\dual\AddressSet{}} = \AddressSet$. We
use $a$ and $b$ to range over elements of $\AddressSet \cup \dual\AddressSet$.

An address is a string $aw$ where $w \in \set{i,l,r}^*$. The dual of an
address is defined as $\dual{(aw)} = \dual{a}w$.

We use $\addressA$ and $\addressB$ to range over addresses, we write $\prefix$
for the prefix relation on addresses and we say that $\addressA$ and $\addressB$
are disjoint if $\addressA \not\prefix \addressB$ and $\addressB
\not\prefix \addressA$.

A type is a formula $\Formula$ paired with an address $\address$ written

We use $S$ and $T$ to range over types and we extend to
types several operations defined on formulas: we use logical connectives to
compose types so that $\FormulaF_{\address l} \mathbin\star \FormulaG_{\address
r} \eqdef (\FormulaF \mathbin\star \FormulaG)_\address$ and
$\sigma\X.\Formula_{\address i} \eqdef (\sigma\X.\Formula)_\address$; the dual
of a type is obtained by dualizing both its formula and its address, that is
$\dual{(\Formula_\address)} \eqdef \dual\Formula_{\dual\address}$; type
substitution preserves the address in the type within which the substitution
occurs, but forgets the address of the type being substituted, that is
$\FormulaF_\addressA\subst{\FormulaG_\addressB}\X \eqdef
\FormulaF\subst\FormulaG\X_\addressA$.

We often omit the address of constants (which represent terminated
conversations) and we write $\strip{S}$ for the formula obtained by forgetting
the address of $S$. Finally, we write $\tred$ for the least reflexive relation
on types such that $S_1 \star S_2 \tred S_i$ and $\sigma\X.S \tred

Consider once again the formula $\FormulaF \eqdef \tmu\X.X \plinchoice \One$ that
describes the behavior of buyer (<Ref>) and let
$a$ be an arbitrary atomic address. We have

\[
\Formula_a
\tred (\Formula \plinchoice \One)_{ai}
\tred \Formula_{ail}
\tred (\Formula \plinchoice \One)_{aili}
\tred \One_{ailir}
\]

where the fact that the types in this sequence all share a common non-empty
prefix `$a$' indicates that they belong to the same conversation.

Note how the symbols $i$, $l$ and $r$ composing an address indicate the step
taken in the syntax tree of types for making a move in this sequence: $i$
means “inside”, when a fixed point operator is unfolded, whereas $l$ and
$r$ mean “left” and “right”, when the corresponding branch of a
connective is selected.

§ CALCULUS

In this section we define syntax and reduction semantics of , a variant of
the linear $\pi$-calculus [Kobayashi et al., 1999] in which all channels
are meant to be used for exactly one communication. The calculus supports
(co)recursive data types built using units, pairs and disjoint sums. These data
types are known to be the essential ingredients for the encoding of sessions in
the linear
$\pi$-calculus [Kobayashi, 2002, Dardha et al., 2017, Scalas et al., 2017].

§.§ Syntax of Processes

§.§ Operational Semantics

§ TYPE SYSTEM

In this section we present the typing rules for .

As usual we introduce typing contexts to track the type of the names occurring
free in a process. A typing context is a finite map from names to types
written $x_1 : S_1, \dots, x_n : S_n$. We use $\CtxC$ and $\CtxD$ to
range over contexts, we write $\dom\Ctx$ for the domain of $\Ctx$ and
$\Ctx,\CtxD$ for the union of $\Ctx$ and $\CtxD$ when
$\dom\Ctx \cap \dom\CtxD = \emptyset$.

Typing judgments have the form $\qtp\Ctx{P}$ and we say that $P$ is quasi
typed in $\Ctx$.
For the time being we say “quasi typed” and not “well typed” because some
infinite derivations using the rules in <Ref> are invalid.
Well-typed processes are quasi-typed processes whose typing derivation satisfies
some additional validity conditions that we detail in <Ref>.

§.§ Typing Rules

§.§ From Quasi Typed to Well Typed Processes

§.§ Examples

§ CORRECTNESS

In this section we present the proof of <Ref>.
In general, the proof technique follows again that presented in
<Ref>. However, the different scenario
implies different design choices. Hence, we think that it is worth
showing a more detailed sketch of the proof of <Ref> by introducing
the main intermediate results and by relating them to .
Then, as in <Ref>, we present all the detailed proofs.

§.§ Proof Sketch

§.§ Subject Reduction

§.§ Proximity and Multicuts

§.§ Additional Properties

§.§ Soundness

§ COMPARING THE TYPE SYSTEMS

This last section concludes <Ref> so we dedicate it to a comparison
between the two approaches to fair termination that we presented, that is,
the session based one (see <Ref>) and that about linear logic
(in the present chapter).

The most important result is that the two approaches cannot be actually compared
since there exist examples that are accepted in the former and rejected in the other and viceversa.
Here we provide two examples of this fact (see <Ref>).

Then, such result leaves an open problem, that is establishing the meaning of fair subtyping
in the linear logic scenario. Indeed, the type system in <Ref> does not
use subtyping.
What makes this research line interesting is how infinite behaviors are dealt with
in the two approaches; the former relies on fair subtyping and the second on validity conditions.

To conclude, in <Ref> we encode <Ref> in the linear logic
context and we see how it is rejected by the type system in <Ref>.

Here we recall the forwarder that we proved to be well typed in in <Ref>.
We model the same process using binary sessions and we try to prove that it is well typed
using the type system in <Ref>.

\[
\Forwarder(x,y) = \x\iact
\set{\lok.\y\oact\lok.\Call{\Forwarder}{\x,\y},
\lstop.\y\oact\lstop.\Wait{x}{\Close\y}
\]

where $\x$ and $\y$ are used according to $S_x$ and $S_y$ defined below

\[
\begin{array}{lr}
S_x = \In\set{\lok.S_x,\lstop.\End[\In]}
& \qquad
S_y = \Out\set{\lok.S_y,\lstop.\End[\Out]}
\end{array}
\]

It is clear that, if we try to provide a typing derivation for $\Forwarder$, then
we have to apply rule tb-tag that we report here for the sake of clarity.

\[
\inferrule
{\forall i\in I: \wtp[n]{\Ctx, x : S_i}{P_i}}
\textstyle
\wtp[n]{\Ctx, x : \Pol\set{\l_i : S_i}_{i \in I}}
{x\Pol\set{\l_i : P_i}_{i \in I}}
\]

In order to apply such rule the branches must be typed in some
contexts that differ only with respect to $\x$.
Hence, we cannot apply tb-tag by taking into account $S_x$ and $S_y$
because the behavior of $\y$ changes as well.
We can try to solve the problem by placing casts in the right positions

\[
\Forwarder(x,y) = \x\iact
\set{\lok.\Cast\y\y\oact\lok.\Call{\Forwarder}{\x,\y},
\lstop.\Cast\y\y\oact\lstop.\Wait{x}{\Close\y}
\]

Indeed $\y$ is used according to $\Out\lok.S_y$ and $\Out\lstop.\End[\Out]$
in the left and right branches, respectively. Moreover,
the two applications of fair subtyping are correct and we can easily derive
$S_y \subt[1] \Out\lok.S_y$ and $S_y \subt[1] \Out\lstop.\End[\Out]$.
Note that the weights are $1$ because the types differ only on the topmost
output, which means that the contravariant rule fsb-tag-out-2 for
output must be applied.

Now we can try to provide a typing derivation (we omit the rule names).

\[
\begin{prooftree}
\[
\[
\[
\vdots
\justifies
\wtp[n]{\x : S_x , \y : S_y}{\Call{\Forwarder}{\x,\y}}
\]
\justifies
\wtp[n]{\x : S_x , \y : S_y}{\y\oact\lok.\Call{\Forwarder}{\x,\y}}
\]
\justifies
\wtp[n+1]{\x : S_x , \y : \Out\lok.S_y}{\Cast\y\y\oact\lok.\Call{\Forwarder}{\x,\y}}
\]
\[
\[
\[
\[
\justifies
\wtp[n]{\y : \End[\Out]}{\Close\y}
\]
\justifies
\wtp[n]{\x : \End[\In] : \y : \End[\Out]}{\Wait{\x}{\Close\y}}
\]
\justifies
\wtp[n]{\x : \End[\In], \y : \Out\lstop.\End[\Out]}{\oact\lstop\dots}
\]
\justifies
\wtp[n+1]{\x : \End[\In], \y : S_y}{\Cast\y\dots}
\]
\justifies
\wtp[n+1]{\x : S_x, \y : S_y}{\Call{\Forwarder}{\x,\y}}
\end{prooftree}
\]

where the right branch ends with an application of tb-end which assigns rank $n$.
Indeed, tb-tag requires that the rank is an upper bound to the rank of the
branches so we assign it in order to match that of the left one.
Note that it is not possible to assign a finite rank to the process
because it requires $n = n+1$, hence the process if cast unbounded (<Ref>).

[A Hopeful Player]

The slot machine was a recurring example in <Ref> (see <Ref>).
In <Ref> we described the behaviors of a fair and an unfair machine.
The second one simply never lets the player win. Let $S$, $T$ be
the types from <Ref> such that

\[
\begin{array}{rcl}
S & = & \In\tplay.(\Out\twin.S + \Out\tlose.S) + \In\tquit.\End[\Out]
\\
T & = & \In\tplay.\Out\tlose.T + \In\tquit.\End[\Out]
\end{array}
\]

Now we can model the two implementations of the machines. For the sake of simplicity,
we adapt the one in <Ref> to the binary case. We dub $\SlotMachineF$ the fair
machine and $\SlotMachineU$ the unfair one.

\[
\begin{array}{rcl}
\SlotMachineF(x) & \peq &
\x\iact\set{
\tplay.\x\oact\set{
\twin.\pinvk\SlotMachineF{x},
\tlose.\pinvk\SlotMachineF{x}
\tquit.\pclose{x}
\\
\SlotMachineU(x) & \peq &
\x\iact\set{
\tplay.\x\oact\tlose.\pinvk\SlotMachineU{x},
\tquit.\pclose{x}
\end{array}
\]

It is easy to see that $\wtp[0]{\x : S}{\pinvk\SlotMachineF{x}}$ and
that $\x : S \not\vdash \pinvk\SlotMachineU{x}$ since the $\twin$ branch is missing.
We can try to rewrite $\SlotMachineU$ in order to be well-typed with $\x : S$.
First, we can place a cast in the $\tlose$ branch.

\[
\SlotMachineU(x) \peq
\x\iact\set{
\tplay.\pcast\x\x\oact\tlose.\pinvk\SlotMachineU{x},
\tquit.\pclose{x}
\]

where the cast is correct since we can derive
$(\Out\twin.S + \Out\tlose.S) \subt[1] \Out\tlose.S$. The $1$ weight
is due to the fact that the two types differ only for the topmost output, which requires
an application of fsb-tag-out-2.
Let us try to derive a typing judgment.

\[
\begin{prooftree}
\[
\[
\[
\vdots
\justifies
\wtp[n]{\x : S}{\pinvk\SlotMachineU{x}}
\]
\justifies
\wtp[n]{\x : \Out\tlose.S}{\x\oact\tlose.\pinvk\SlotMachineU{x}}
\]
\justifies
\wtp[n+1]{\x : \Out\twin.S + \Out\tlose.S}{\pcast\x\x\oact\tlose.\pinvk\SlotMachineU{x}}
\]
\[
\justifies
\wtp[n+1]{x : \End[\Out]}{\pclose\x}
\]
\justifies
\wtp[n+1]{\x : S}\pinvk\SlotMachineU{x}
\end{prooftree}
\]

Hence, we cannot find a finite rank; the process is cast unbounded (see <Ref>).

Alternatively we can try to place a cast before the first invocation of the process since it is clear
that $\SlotMachineU$ uses $\x$ according to $T$. Such cast would be invalid
since in <Ref> we proved that $S \not\subt T$.
Hence, the only typing judgment that we can derive is $\wtp[0]{\x : T}{\pinvk\SlotMachineU{x}}$.

Now we can apply the same reasoning from the point of view.
Let us model the fair (<Ref>) and the unfair machines.
We dub $\MachineF$ the fair machine and $\MachineU$ the unfair one.

\[
\begin{array}{rcl}
\MachineF(x,y) & \peq & \Corec\x.
\\ & &
\Case\x{
\PiChoice{
\Select\WinTag\x.\Call\MachineF{x,y}
\Select\LoseTag\x.\Call\MachineF{x,y}
\PiWait\x.\PiClose\y
\\
\MachineU(x,y) & \peq & \Corec\x.
\Case\x{
\Select\LoseTag\x.\Call\MachineU{x,y}
\PiWait\x.\PiClose\y
\end{array}
\]

In <Ref> we proved that
$\qtp{x : \FormulaG_b, y : \One}{\Call\MachineF{x,y}}$ and that $\MachineF$ is well-typed
where $\FormulaG \eqdef \tnu\X.(X \plinchoice X) \plinbranch \Bot$.
At the same time we can prove that $\qtp{x : \FormulaG_b, y : \One}{\Call\MachineU{x,y}}$

\[
\begin{prooftree}
\[
\[
\[
\mathstrut\smash\vdots
\justifies
\qtp{
x : \FormulaG_{bilr},
y : \One
\Call\MachineU{x,y}
\]
\justifies
\qtp{
x : \FormulaG'_{bil},
y : \One
\Select\LoseTag\x.\Call\MachineU{x,y}
\using\refrule[select]\SelectRule
\]
\[
\[
\justifies
\qtp{
y : \One
\PiClose\y
\using\refrule[close]{\PiCloseRule}
\]
\justifies
\qtp{
x : \Bot,
y : \One
\PiWait\x.\PiClose\y
\using\refrule[wait]{\PiWaitRule}
\]
\justifies
\qtp{
x : (\FormulaG' \plinbranch \Bot)_{bi},
y : \One
\Case\x{
\Select\LoseTag\x.\Call\MachineU{x,y}
\PiWait\x.\PiClose\y
\using\refrule[case]{\CaseRule}
\]
\justifies
\qtp{
x : \FormulaG_b,
y : \One
\Call\MachineU{x,y}
\using\refrule[corec]{\CorecRule}
\end{prooftree}
\]

Moreover the process is well-typed since no choices are met.
This example points out that we can type two different processes with the same type
while in the session scenario we the correspondence between types and processes is

Now we can focus on the player side and we can try to model a hopeful player
that plays until it receives $\WinTag$. In that case, it stops playing.
We first write it in the binary session scenario and then we encode it
in .

\[
\Play(\x) \peq \x\oact\tplay.\x\iact\set{\twin.\pclose\x,\tlose.\pinvk\Play\x}
\]

where $\x$ is used according to $T_p = \Out\tplay.\In\set{\twin.\End[\Out], \tlose.T_p}$.
It can be derived that $\wtp[0]{\x : T_p}{\pinvk\Play\x}$.
Note that the system consisting of $\MachineF$ and $\Play$ is fairly terminating.
Indeed $S \compatible T_p$.

Now we model the same process in . In particular,
we slightly modify the player in <Ref>.

\[
\Player(x) =
\Rec\x.
\Select\PlayTag\x.
\Case\x{
\Call\Player\x
\Rec\x.\Select\QuitTag\x.\PiClose\x
\]

Let us look at the typing derivation with $\FormulaF \eqdef \tmu\X.(X \plinbranch X) \plinchoice \One$.

\[
\begin{prooftree}
\[
\[
\[
\mathstrut\smash\vdots
\justifies
\qtp{
x : \FormulaF_{aill}
\Call\Player\x
\]
\qquad
\[
\[
\[
\justifies
\qtp{
x : \One
\PiClose\x
\using\refrule[close]{\PiCloseRule}
\]
\justifies
\qtp{
x : \Formula'_{ailri}
\Select\QuitTag\x.\PiClose\x
\using\refrule[select]{\SelectRule}
\]
\justifies
\qtp{
x : \FormulaF_{ailr}
\Rec\x.\Select\QuitTag\x.\PiClose\x
\using\refrule[rec]{\RecRule}
\]
\justifies
\qtp{
x : (\FormulaF \plinbranch \FormulaF)_{ail}
\Case\x{
\Call\Player\x
\Rec\x\Select.\QuitTag\x.\PiClose\x
\using\refrule[case]{\CaseRule}
\]
\justifies
\qtp{
x : \Formula'_{ai}
\Select\PlayTag\x.
\Case\x{
\Call\Player\x
\Rec\x.\Select\QuitTag\x.\PiClose\x
\using\refrule[select]{\SelectRule}
\]
\justifies
\qtp{
x : \Formula_a
\Call\Player\x
\using\refrule[rec]{\RecRule}
\end{prooftree}
\]

Note that now $\rankof{\Call\Player\x} = 0$ since there are no choices.
Hence, the infinite branch is fair because it traverses no choices.
We can conclude that the $\Call\Player\x$ is not well typed because
because the infinite, fair branch is not valid.
We recall that the player in <Ref> was well typed because
the infinite branch was unfair as it contained infinitely many finitely ranked choices.

<Ref> show that the type systems in <Ref> cannot be compared
to that in <Ref>. <Ref> illustrates a process that can be only typed in while <Ref> show a process that can be typed only in the session based calculi.

Moreover <Ref> shows a peculiar difference between the type systems.
In <Ref> the tight correspondence between types and processes allows us
to use a fair type to prove that a fair process is well-typed.
Such correspondence does not hold in as we proved that both the fair and the unfair
slot machines can be typed with the same formula.

We conclude this section showing how to encode delegation in and trying
to encode <Ref> to see whether it is accepted or rejected in .

We show delegation how can be encoded in .
[Lindley and Morris, 2015] provide an encoding from GV (a session typed functional language) to (a process calculus based on classical linear logic).
Hence, they encode (binary) session types
to the types of CP, that is, linear logic formulas. Concerning delegation, the encoding
is provided as

\[
\begin{array}{rclrcl}
\enc{\Out\T.\S} & = & \co{\enc\T} \tfork \enc\S
& \qquad
\enc{\In\T.\S} & = & \enc\T \tjoin \enc\S
\end{array}
\]

(see <cit.>).
Following the encoding of types we extend the encoding to
the processes in <Ref>.

\[
\begin{array}{rclrcl}
\enc{\POutput\x{(\y)}.P} & = & \Fork\x\z{\Link\y\z}{\enc{P}}
& \qquad
\enc{\PInput\x{(\y)}} & = & \Join\x\y{\enc{P}}
\end{array}
\]

In this example we encode <Ref> in and we see if we obtain a well-typed process or not.
To encode delegation we refer to <Ref>.
Let us first recall the process and the main types.

\[
\begin{array}{@{}r@{~}l@{}}
& \NewPar\y{\NewPar\x{\Call A {x,y}}{\Call B x}}{\Call B y}
\\
\Definition{A}{x,y}{& \POutput\x\lmore.\POutput\x\y.\Call B x}
\\
\Definition{B}{x}{&
\PRecv\x{
\lmore : \PInput\x{(y)}.\Call A {y,x},
\lstop : \Wait\x\Done
\end{array}
\]

where $\x$ and $\y$ are used according to $S_A$ and $T_A$ in $A(x,y)$ and
$\x$ is used according to $S_B$ in $B(x)$.

\[
\begin{array}{rcl}
S_A & = & \Out\lmore.\Out\T_A.S_B
\\
S_B & = & \In\lmore.\In\S_A.T_A \branch \In\lstop.\End[\In]
\\
T_A & = & \Out\lmore.\Out\T_A.S_B \choice \Out\lstop.\End[\Out]
\end{array}
\]

Now we can look at the encoding of processes.

\[
\begin{array}{rcl}
\enc{A(x,y)} & = & \Rec\x.\Select\lmore\x.\Fork\x\z{\Link\y\z}{\enc{B(\x)}}
\\
\enc{B(x)} & = & \Corec\x.\Case\x{\Join\x\y\enc{A(y,x)}}{\PiWait\x}
\end{array}
\]

The encoding of types is more involved. Since we do not have subtyping in
, we can encode $S_b$ and $T_A$. Moreover, if we replace $\In{S_A}.T_A$
with $\In{T_A}.T_A$ in $S_B$, we obtain that $\co{S_B} = T_A$.
Let $\enc{T_A} = \Formula_A$ and $\enc{S_B} = \Formula_B$.

\[
\begin{array}{rlr}
\Formula_A = & \tmu\Y.(\dual{\Formula_A} \tfork \Formula_B) \plinchoice \One
\\ & \hfill \text{by definition of $\enc{T_A}$}
\\ 			 = & \tmu\Y.(\dual{\Formula_A} \tfork ((\Y \tjoin \Y) \plinbranch \Bot)) \plinchoice \One
\\ & \hfill \text{by replacing $\Formula_B$}
\\			 = & \tmu\Y.((\tnu\X.(\Y \tjoin ((\X \tfork \X) \plinchoice \One)) \plinbranch \Bot)
\tfork ((\Y \tjoin \Y) \plinbranch \Bot)) \plinchoice \One \qquad
\\ & \hfill \text{by replacing $\dual{\Formula_A}$}
\\
\Formula_B = & \tnu\X.(\Formula_A \tjoin \Formula_A) \plinbranch \Bot
\\ & \hfill \text{by definition of $\enc{S_B}$}
\\
= & \tnu\X.(\Formula_A \tjoin ((\X \tfork \X) \plinchoice \One)) \plinbranch \Bot
\\ & \hfill \text{by replacing $\Formula_A$}
\\
= & \tnu\X.((\tmu\Y.(\X \tfork ((\Y \tjoin \Y) \plinbranch \Bot)) \plinchoice \One)
\tjoin ((\X \tfork \X) \plinchoice \One)) \plinbranch \Bot
\\ & \hfill \text{by replacing $\Formula_A$}
\end{array}
\]

From these definition it can be noted that it the encoding is not straightforward since we do not
know how/when actually unfold the formulas. Indeed we are not able to find the right
types to prove that the process is quasi-typed.

Furthermore, assuming that we could find such types, it would turn out that $B$ is well-typed
while $A$ is not as its infinite thread in not a $\nu$ one.

§ RELATED WORK

On account of the known encodings of sessions into the linear
$\pi$-calculus [Kobayashi, 2002, Dardha et al., 2017, Scalas et al., 2017],
belongs to the family of process calculi providing logical foundations to
sessions and session types. Some representatives of this family are
[Caires et al., 2016] and its variant equipped with a circular
proof theory [Derakhshan and Pfenning, 2019, Derakhshan, 2021], [Wadler, 2014] and
[Lindley and Morris, 2016], among others.

There are two main aspects distinguishing from these calculi. The first
one is that these calculi take sessions as a native feature. This fact can be
appreciated both at the level of processes, where session endpoints are
linearized resources that can be used multiple times albeit in a
sequential way, and also at the level of types, where the interpretation of the
$\FormulaF \tfork \FormulaG$ and $\FormulaF \tjoin \FormulaG$ formulas is skewed
so as to distinguish the type $\FormulaF$ of the message being sent/received on
a channel from the type $\FormulaG$ of the channel after the exchange has taken

In contrast, adopts a more fundamental communication model based on
linear channels, and is thus closer to the spirit of the encoding of
linear logic proofs into the $\pi$-calculus proposed by [Bellin and Scott, 1994]
while retaining the same expressiveness of the
aforementioned calculi. To some extent, is also more general than those
calculi, since a formula $\FormulaF \tfork \FormulaG$ may be interpreted as a
protocol that bifurcates into two independent sub-protocols $\FormulaF$ and
$\FormulaG$ (we have seen an instance of this pattern in
<Ref>). So, is natively equipped with the
capability of modeling some multiparty interactions, in addition to all of the
binary ones.

A session-based communication model identical to , but whose type system
is based on intuitionistic rather than classical linear logic, has been
presented by [DeYoung et al., 2012]. In that work,
the authors advocate the use of explicit continuations with the purpose of
modeling an asynchronous communication semantics and they prove the equivalence
between such model and a buffered session semantics. However, they do not draw a
connection between the proposed calculus and the linear
$\pi$-calculus [Kobayashi et al., 1999] through the encoding of binary
sessions [Kobayashi, 2002, Dardha et al., 2017] and, in the type system,
the multiplicative connectives are still interpreted asymmetrically.

The second aspect that distinguishes from the other calculi is its type
system, which is still deeply rooted into linear logic and yet it ensures fair
termination instead of
progress [Caires et al., 2016, Wadler, 2014, Qian et al., 2021],
termination [Lindley and Morris, 2016] or strong
progress [Derakhshan and Pfenning, 2019, Derakhshan, 2021]. Fair termination entails
progress, strong progress and lock freedom [Kobayashi, 2002, Padovani, 2014], but at
the same time it does not always rule out processes admitting infinite
executions. Simply, infinite executions are deemed unrealistic because they are

Another difference between and other calculi based on linear logic is
that its operational semantics is completely ordinary, in the sense that it does
not include commuting conversions, reductions under prefixes, or the swapping of
communication prefixes. The cut elimination result of , on which the
proof of <Ref> is based, works by reducing cuts from the bottom
of the derivation instead of from the
top [Baelde et al., 2016, Doumane, 2017, Baelde et al., 2022]. As a consequence, it is
not necessary to reduce cuts guarded by prefixes or to push cuts deep into the
derivation tree to enable key reductions in processes.

The extension of calculi based on linear logic with non-deterministic features
has recently received quite a lot of attention. [Rocha and Caires, 2021] have proposed
a session calculus with shared cells
and non-deterministic choices that can model mutable state. Their typing rule
for non-deterministic choices is the same as our own, but in their calculus
choices do not reduce. Rather, they keep track of every possible evolution of a
process to be able to prove a confluence result.

[Qian et al., 2021] introduce coexponentials, a new
pair of modalities that enable the modeling of concurrent clients that compete
in order to interact with a shared server that processes requests sequentially.
In this setting, non-determinism arises from the unpredictable order in which
different clients are served. Interestingly, the coexponentials are derived by
resorting to their semantics in terms of least and greatest fixed points. For
this reason, the cut elimination result of might be useful to attack the
termination proof in their setting.

[Agda Mechanizations]Agda Mechanizations
(Allegro Moderato)

CHAPTER: A LIBRARY FOR (GENERALIZED) INFERENCE SYSTEMS

In this chapter we present a library for supporting generalized inference systems (see <Ref>) in Agda [The Agda Team, 2022].
Summarizing from <Ref>,
an inference system [Aczel, 1977, Leroy and Grall, 2009, Sangiorgi, 2011], that is, a set of (meta-)rules stating that
a consequence can be derived from a set of premises, is a simple, general and widely-used way to express
and reason about a recursive definition. In most cases such recursive definition is seen as inductive,
that is,  the denoted set consists of the elements with a finite derivation.
This  enables inductive reasoning, that is, to prove that the elements an inductively
defined set satisfy a property, it is enough to show that, for each (meta-)rule, the property
holds for the consequence assuming that it holds for the premises.
In other cases, the recursive definition is seen as coinductive,
that is, the denoted set  consists of the elements with a possibly infinite derivation.
This enables coinductive reasoning, that is, to prove that all the elements satisfying a
property belong to the coinductively defined set, it is enough to show that, when the property
holds for an element, it can be derived from premises for which the property holds as well.
Recently, a generalization of inference systems has been proposed [Ancona et al., 2017, Dagnino, 2019, Dagnino, 2021]
which handles cases where neither the inductive, nor the purely coinductive intepretation provides the desired meaning.
This approach is called flexible coinduction, and, correspondingly, coinductive reasoning is
generalized as well by a principle which is called bounded coinduction.

The Agda proof assistant [The Agda Team, 2022] offers language constructs to inductively/coinductively define predicates,
and correspondingly  built-in proof principles.
However, in this way the recursive definition is monolithic, and hard-wired with its chosen interpretation.

In [Ciccone, 2020] we deeply investigated the built-in features of Agda by
inspecting all the different ways a (co)inductive predicate can be defined.
We found out that, while pure (co)inductive definitions are easily supported, a predicate mixing
both approaches led to complex codes with many duplicated notions due to the lack
of modularity (see <Ref>).

Our aim, instead, is to provide an Agda library allowing  the user to express a recursive definition
as an instance of a parametric type of inference systems.
In this way, the user is not committed from the beginning to a given interpretation but, rather,
gets for free a bunch of properties which have been proved once and for all, including the inductive and
coinductive intepretation and the corresponding proof principles.
Moreover, it is possible to define composition operators on inference systems,
for instance union and restriction.
Finally, flexible coinduction is modularly obtained as well,
by composing in a certain way the interpretations of two inference systems.

Indexed containers [Altenkirch et al., 2015] provide a way to specify possibly recursive definitions
of predicates independently from their interpretation and are supported in the Agda standard library.
An Agda implementation of inference systems can be provided by seeing them as indexed containers.
However, this approach requires to structure definitions in an unusual way.
Indeed, inference systems are usually presented through a (finite) set of meta-rules,
denoting all the rules which can be obtained by instantiating meta-variables with values satisfying the side condition.
Hence, we provide a different implementation following this schema, to allow users to write their own inference
system in an Agda format which closely resembles  that “on paper”.
We then prove that the two implementations are equivalent, showing that every  indexed container can be
encoded in terms of meta-rules and viceversa.

It is important to point out that the material presented in <Ref>
holds as long as Agda is consistent.
During the development of the notions we are going to present, Agda received many updates.
As an example, an inconsistency in mixing sized types and coinductive records
has been found.

The library is available on GitHub (see [Ciccone et al., 2021]) and has been tested
with the Agda 2.6.2.2. In case of future Agda updates, we will try to keep the
material updated.

The chapter is structured as follows.
In <Ref> we show the mechanization of the meta theory of (generalized) inference systems (see <Ref>).
In particular, we present the main datatypes to encode inference systems in Agda, how to obtain their interpretations and,
most important, the proof principles. We provide the formalization of the examples that we introduce in <Ref> since
they give an overview of all the features of the library.
Then, in <Ref> we show a more involved example, that is, a lambda calculus with divergence and
we prove soundness and completeness of its big-step semantics.
At last, in <Ref> we investigate the relation between inference systems and indexed containers
[Altenkirch et al., 2015] that are supported by the standard library.

§ META THEORY

In this section we describe the main definitions of the library.
Concerning the meta-theory, the reader can refer to <Ref>.
Notably, we first present an approach mimicking meta-rules. Then we introduce
the notions of interpretations and we prove the principles.
At last, we formalize the examples we presented in <Ref>.

§.§ (Meta-)Rules/Inference System

§.§ Interpretations and Principles

§.§ Basic Examples

§ DIVERGENCE IN THE LAMBDA-CALCULUS

_1  _2
_1 _2[app]
_1 _2∞[l-div]
_1  _2∞
_1 _2∞[r-div]

$\lambda$-calculus: syntax and big-step semantics

In <Ref> we formalized some basic examples to explain how
the library can be used. In this section we describe a more significant example of instantiation:
an inference system with corules providing a big-step semantics of lambda-calculus including divergence
among the possible results [Ancona et al., 2017], reported in <Ref>.
In this example, corules play a key role: indeed , considering, e.g., the divergent term
$\Omega=\AppExp{(\LambdaExp{\x}{\x$ $\x})}{(\LambdaExp{\x}{\x$ $\x})}$, in the standard inductive big-step
semantics no result can be derived (an infinite proof tree is needed), as for a stuck term;
in the purely coinductive interpretation, any judgment $\eval{\Omega}{\infval}$ would be obtained [Leroy and Grall, 2009].
Since each node of the infinite proof tree for a judgment should also have a finite proof
tree using the corules, the coaxiom coa forces to obtain only $\infty$ as result,
see [Ancona et al., 2017] for a more detailed explanation.
[Other examples of big-step semantic definitions with
more sophisticated corules are given in [Ancona et al., 2018, Ancona et al., 2020].]

In rule app, $\infval$ is used for the result, so the rule also covers the case
when the evaluation of the body of the lambda abstraction diverges.
As usual, $\lamsubst{\te}{\x}{\val}$ denotes capture-avoiding substitution.
Rules l-div and r-div cover the cases when either $\te_1$ or $\te_2$ diverges,
assuming  a left-to-right evaluation strategy.

Terms, values, and results are inductively defined, hence encoded by Agda datatypes.
As customary in implementations of lambda-calculus, we use the De Bruijn notation:
notably, Term n is the set of terms with n free variables.

data Term (n : $\N$) : Set where
var : Fin n $\rightarrow$ Term n
lambda : Term (suc n) $\rightarrow$ Term n
app : Term n $\rightarrow$ Term n $\rightarrow$ Term n

data Value : Set where
lambda : Term 1 $\rightarrow$ Value

term : Value $\rightarrow$ Term 0
term (lambda x) = lambda x

data Value$^\infty$ : Set where
res : Value $\rightarrow$ Value$^\infty$
$\infty$ : Value$^\infty$

The universe consists of big-step judgments (pairs consisting of a term and a result).
The two inference systems of rules and corules are encoded below.

U : Set
U = Term 0 $\times$ Value$^\infty$

data BigStepRN : Set where val app l-div r-div : BigStepRN
data BigStepCoRN : Set where COA : BigStepCoRN

BigStepIS : IS U
BigStepIS .Names = BigStepRN
BigStepIS .rules val = from val$\textrm{-}$r
BigStepIS .rules app = from app$\textrm{-}$r
BigStepIS .rules L$\textrm{-}$DIV = from l$\textrm{-}$div$\textrm{-}$r
BigStepIS .rules R$\textrm{-}$DIV = from r$\textrm{-}$div$\textrm{-}$r

BigStepCoIS : IS U
BigStepCoIS .Names  = BigStepCoRN
BigStepCoIS .rules COA = from coa$\textrm{-}$r

where BigStepRN are the rule names, and each rule name has an associated element of FinMetaRule U.
For instance, app$\textrm{-}$r is given below.
The auxiliary function subst, omitted, implements capture-avoiding substitution.

app$\textrm{-}$r : FinMetaRule U
app$\textrm{-}$r .Ctx = Term 0 $\times$ Term 1 $\times$ Term 0 $\times$ Value $\times$ Value$^\infty$
app$\textrm{-}$r .comp (t1 , t , t2 , v , v$^\infty$) =
(t1 , res (lambda t)) :: (t2 , res v) ::
(subst t (term v) , v$^\infty$) :: [] ,
(app t1 t2 , v$^\infty$)

The big-step semantics can be obtained as the interpretation of the generalized inference system,
as shown below. We use the flavour with thunks.

_$\Downarrow$_ : Term 0 $\rightarrow$ Value$^\infty$ $\rightarrow$ Size $\rightarrow$ Set
(t $\Downarrow$ v$^\infty$) i = SFCoInd$\llbracket$ BigStepIS , BigStepCoIS $\rrbracket$ (t , v$^\infty$) i

_$\Downarrow_\textrm{i}$_ : Term 0 $\rightarrow$ Value$^\infty$ $\rightarrow$ Set
t $\Downarrow_\textrm{i}$ v$^\infty$ = Ind$\llbracket$ BigStepIS $\cup$ BigStepCoIS $\rrbracket$ (t , v$^\infty$)

The second predicate  (i stands for “inductive”)  models that a judgment has a finite proof tree in the
inference system consisting of rules and coaxiom, and will be used in proofs.

$\lambda$-calculus: small-step semantics

Small-step semantics, reported in <Ref>, can also be obtained appropriately instantiating the library.
In this case, the universe consists of small-step judgments, which are pairs of terms.
There is only one inference system, where SmallStepRN are the rule names,
and each rule name has an associated element of FinMetaRule U.

U : Set
U = Term 0 $\times$ Term 0

data SmallStepRN : Set where $\beta$ L$\textrm{-}$app R$\textrm{-}$app : SmallStepRN

SmallStepIS : IS U
SmallStepIS .Names = SmallStepRN
SmallStepIS .rules $\beta$ = from $\beta\textrm{-}$r
SmallStepIS .rules L$\textrm{-}$app = from l$\textrm{-}$app$\textrm{-}$r
SmallStepIS .rules R$\textrm{-}$app = from r$\textrm{-}$app$\textrm{-}$r

For instance, $\beta\textrm{-}$r is given below.

$\beta\textrm{-}$r : FinMetaRule U
$\beta\textrm{-}$r .Ctx = Term 1 $\times$ Value
$\beta\textrm{-}$r .comp (t , v) =
[] ,
(app (lambda t) (term v) , subst t (term v))

The one-step relation $\Rightarrow$ is obtained as the inductive interpretation of the (standard) inference system.
Then, finite computations are modeled by its reflexive and transitive closure $\Rightarrow^\star$,
defined using Star in the Agda library,  as shown below.

_$\Rightarrow$_ : Term 0 $\rightarrow$ Term 0 $\rightarrow$ Set
t $\Rightarrow$ t' = Ind$\llbracket$ SmallStepIS $\rrbracket$ (t , t')

_$\Rightarrow^\star$_ : Term 0 $\rightarrow$ Term 0 $\rightarrow$ Set
_$\Rightarrow^\star$_ = Star _$\Rightarrow$_

Infinite computations, instead, are modeled by the relation $\Rightarrow^\infty$,
coinductively defined by the meta-rule

\[
\inferrule{\te'\Rightarrow^\infty}{\te\Rightarrow^\infty}{\te\Rightarrow\te'}
\]

that we encoded in Agda by using thunks.

data _$\Rightarrow^\infty$ : Term 0 $\rightarrow$ Size $\rightarrow$ Set where
step : $\forall$ t t' i $\rightarrow$ t $\Rightarrow$ t' $\rightarrow$ Thunk (t' $\Rightarrow^\infty$) i $\rightarrow$ t $\Rightarrow^\infty$ i

The proof of equivalence between big-step and small-step semantics is structured as follows,
where $\Spec=\{\Pair{\te}{\val}\mid\te\Rightarrow^\star\val\}\cup\{\Pair{\te}{\infty}\mid\te\Rightarrow^\infty\}$.

$\eval{\te}{\val}$ implies $\te\Rightarrow^\star\val$ We use fcoind$\texttt{-}$to$\texttt{-}$ind (see <Ref>),
and then reason by induction on the judgment $\te{\Downarrow_\textrm{i}}\val$.
That is, we show that $\te\Rightarrow^\star\val$ is closed w.r.t. the inference system consisting of rules and corules.
As already pointed out for the maxElem example, the use of fcoind$\textrm{-}$to$\textrm{-}$ind
in the proof corresponds to the fact that, without the coaxiom coa, unsound judgments would be derived,
e.g., $\eval{\Omega}{\val}$ for $\val\in\Val$.

$\eval{\te}{\infty}$ implies $\te\Rightarrow^\infty$  This implication, instead, would hold even in the purely coinductive case.
It can be proved from progress and subject reduction properties:

Progress $\eval{\te}{\infty}$ implies that there exists $\te'$ such that $\te\Rightarrow\te'$.

Subject reduction $\eval{\te}{\infty}$ and $\te\Rightarrow\te'$ implies $\eval{\te'}{\infty}$.

Completeness By bounded coinduction (see <Ref>).

$\te\Rightarrow^\star\val$ implies $\te{\Downarrow_\textrm{i}}\val$ By induction on the number of steps.

$\te\Rightarrow^\infty$ implies $\te{\Downarrow_\textrm{i}}\infty$ Trivial, since the coaxiom coa can be applied.

Consistency  We have to show that, for each $\Pair{\te}{\infval}\in\Spec$,  $\Pair{\te}{\infval}$
is the consequence of a big-step rule where the premises are in $\Spec$ as well.
We distinguish two cases.

$\te\Rightarrow^\star\val$ By induction on the number of steps. If it is $0$, then $\te$ is a value,
hence we can use rule val. Otherwise, $\te$ is an application, and we can use rule app.

$\te\Rightarrow^\infty$ The term $\te$ is an application $\AppExp{\te_1}{\te_2}.$ We distinguish the following cases:

* $\te_1$ diverges, hence we can use rule l-div

* $\te_1$ converges and $\te_2$ diverges, hence we can use rule r-div

* both $\te_1$ and $\te_2$ converge, hence we can use rule app.

Note that in this proof by cases we need to use the excluded middle principle,
which is defined in the standard library, and  postulated  in our proof.

§ INDEXED (ENDO) CONTAINERS

We conclude this section by investigating the analogies and the differences of
generalized inference systems with respect to index containers.
Indexed containers [Altenkirch et al., 2015] are a rather general notion,
meant to capture families of datatypes with some form of indexing.
They are part of the Agda standard library.
We report below the definition, simplified and adapted a little for presentation purpose.
Notably, we use ad-hoc field names, chosen to reflect the explanation provided below.

record Container $\ell$i $\ell$o
(I : Set $\ell$i) (O : Set $\ell$o) ($\ell$c $\ell$p : Level) : Set _ where
constructor _ $\lhd$ _/_
Cons  : (o : O) $\rightarrow$ Set $\ell$c
Pos : $\forall$ o $\rightarrow$ Cons o $\rightarrow$ Set $\ell$p
input : $\forall$ o (c : Cons o) $\rightarrow$ Pos c $\rightarrow$ I

$\llbracket$_$\rrbracket$: $\forall$ $\ell$i $\ell$o $\ell$c $\ell$p $\ell$ I : Set $\ell$i O : Set $\ell$o $\rightarrow$
Container I O $\ell$c $\ell$p $\rightarrow$
(I $\rightarrow$ Set $\ell$) $\rightarrow$ (O $\rightarrow$ Set _)
$\llbracket$ Cons $\lhd$ Pos / input $\rrbracket$ X o =
$\Sigma$[ c $\in$ C o ] ((p : P c) $\rightarrow$ X (inp c p))

To explain the view of an inference system as an indexed container,
we can think of the latter as describing a family of datatype constructors
where I and O are  input and output sorts,  respectively.
Then, Cons specifies, for each output sort o,
the set of its constructors; for each constructor for o,
Pos specifies a set of positions to store inputs to the constructor; finally,
input specifies the input sort for each position in a constructor.

The function $\llbracket$_$\rrbracket$ models the “semantics” of an indexed container,
that is, given a family of inputs X indexed by I, it returns the family
of outputs indexed by O which can be constructed by providing to
some constructor inputs from P of correct sorts.

Then, inference systems can be defined as indexed containers
where input and output sorts coincide, and are the elements of the universe, as follows.

ISCont : $\ell$c $\ell$p : Level $\rightarrow$ (U : Set $\ell$u) $\rightarrow$ Set _
ISCont $\ell$c $\ell$p U = Container U U $\ell$c $\ell$p

In this way, for each u : U:

* Cons u is the set of (indexes for) all the rules which have consequence u

* Pos c is the set of (indexes for) the premises of the c-th rule

* input c p is the p-th premise of the c-th rule

This view comes out quite naturally observing that an inference system is an element
of $\wp(\wp(\universe)\times\universe)$; equivalently, a function which, for each $\judg\in\universe$,
returns the set of the sets of premises of all the rules with consequence $\judg$.
In a constructive setting such as Agda, the powerset construction is not available, hence we have to use functions.
So, for each element u, we need a type to index all rules with consequence u,
and, for each  rule, a type to index its premises, which are exactly the data of an indexed container.

In other words, this view of inference systems as indexed containers explicitly interprets rules as constructors for proofs.
Moreover, definitions in <Ref> can be easily obtained as instances of analogous definitions
for indexed containers, building on the fact that the inference operator associated with an inference
system turns out to be the semantics $\llbracket$_$\rrbracket$ of the corresponding container.

Whereas this encoding allows reuse of notions and code, a drawback is that information is structured in a
rather different way from that “on paper”; notably, we group together rules with the same consequence,
rather than those obtained as instances of the same “schema”, that is, meta-rule.
For this reason we developed the Agda library mimicking meta-rules.
For instance, the inference system for $\allpos$ would be as follows:

allPosCont : ISCont (Colist $\N$ $\infty$)
allPosCont .Cons [] = $\top$
allPosCont .Cons (x :: xs) = x > 0
allPosCont .Pos [] c = $\bot$
allPosCont .Pos x :: xs c = Fin 1
allPosCont .input x :: xs c zero = xs .force

However, we can prove that the two notions are equivalent, as shown below.
To this end, we define a translation C[_] from inference systems to indexed containers
and a converse translation IS[_].
Note that in the translation C[_] each meta-rule is transformed in all its instantiations;
more precisely, for each u:C, Cons u gives all the instantiations
of meta-rules having u as consequence.
Conversely, in the translation IS[_], each rule is transformed in a meta-rule with trivial context.

C[_] : $\forall$$\ell$c $\ell$p $\ell$n $\rightarrow$ IS $\ell$c $\ell$p $\ell$n U $\rightarrow$ Container U U _ $\ell$p
C[ is ] .Cons u = $\Sigma$[ rn $\in$ is .Names ] $\Sigma$[ c $\in$ is .rules rn .Ctx ]
u $\equiv$ is .rules rn .conclu c
C[ is ] .Pos (rn , _ , refl) = is .rules rn .Pos
C[ is ] .input (rn , c , refl) p = is .rules rn .prems c p

IS[_] : $\forall$$\ell$c $\ell$p $\rightarrow$
Container U U $\ell$c $\ell$p $\rightarrow$ IS zero $\ell$p l $\sqcup$ $\ell$c U
IS[ C ] .Names = $\Sigma$[ u $\in$ U ] C .Cons u
IS[ C ] .rules (u , c) =
Ctx = $\top$ ;
Pos = C .Pos c ;
prems = $\lambda$ _ r $\rightarrow$ C .input c r ;
conclu = $\lambda$ _ $\rightarrow$ u

isf-to-c : $\forall$$\ell$c $\ell$p $\ell$n $\ell$p is : IS $\ell$c $\ell$p $\ell$n U
P : U $\rightarrow$ Set $\ell$p $\rightarrow$ ISF[ is ] P $\subseteq$ $\llbracket$ C[ is ] $\rrbracket$ P
isf-to-c (rn , c , refl , pr) = (rn , c , refl) , pr

c-to-isf : $\forall$l' $\ell$p $\ell$p C : Container U U l' $\ell$p
P : U $\rightarrow$ Set $\ell$p $\rightarrow$ $\llbracket$ C $\rrbracket$ P $\subseteq$ ISF[ IS[ C ] ] P
c-to-isf (c , pr) = (_ , c) , tt , refl , pr

CHAPTER: PROPERTIES OF SESSION TYPES

In this chapter we take into account three interesting properties of binary session types.
All the properties under analysis mix safety and liveness. Hence, we use (<Ref>) as a reference framework
for their definitions and proofs.
Furthermore, for each property we first investigate its safety counterpart and we show how to obtain the desired
one by using corules.
Notably, all the results have been formalized in Agda [Ciccone and Padovani, 2021, Ciccone and Padovani, 2021, Ciccone and Padovani, 2022].
We chose to restrict to the binary case to simplify the mechanizations as much as possible.

The properties that we study are the following:

* Fair Termination of a session type. A fairly terminating session can always eventually
reach termination

* Fair Compliance of two session types. Compliant sessions can always eventually interact to reach
termination (asymmetric variant of <Ref>)

* Fair Subtyping between session types. This property is a compliance-preserving subtyping relation
(see <Ref>)

We begin the chapter by mechanizing in <Ref> the notions presented in <Ref>
and that will be used later.

Then, in <Ref> we introduce an alternative definition of (binary) session
types and its formalization.

Then the chapter is split according to the property under analysis
Furthermore, for each property we show its Agda definition and we explain how
the proof principles (see <Ref>) can be used to prove the correctness.

At last, in <Ref> we
detail the soundness and completeness proof of fair compliance.
The formalization of all the results is available on GitHub [Ciccone and Padovani, 2021].

In this chapter we refer to binary session types but we rely on a syntax
different from the more conventional one presented
in <Ref>. This choice is mainly motivated by the fact we aimed at
simplifying the mechanization as much as possible. In <Ref> we describe all
the advantages of using such representation.

§ FAIR TERMINATION

open import Relation.Nullary using ($\neg$_)
open import Relation.Unary using (Satisfiable; _$\cup$_)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
using (Star)
open import Function.Base using (_$\circ$_)

Imported modules

In this section we mechanize fair termination in its general form, that is,
considering an arbitrary labeled transition system.
In particular, we mechanize the definitions and the notions that we presented in <Ref>.
We will instanciate such property in <Ref> in session based scenarios.
Notably, the entire development is available on GitHub (see [Padovani, 2022]).

The codes that we present takes advantage of many features from the standard library.
<Ref> illustrates the modules that are imported and used in the formalization in this section.
Satisfiable P holds when a proof of P can be exhibited whereas
Star is used to obtain the reflexive transitive closure of the reference relation.
$\neg$ P is equivalent to P $\rightarrow$ $\bot$.
For more details see [Padovani, 2022].

First, we have to consider an arbitrary labelled transition system. Hence
the Agda module is parametric on

(State : Set) (_$\sim>$_ : State $\rightarrow$ State $\rightarrow$ Set)

that is, a set of states and a transition relation.
Then, we define the reflexive transitive closure of the transition relation and the set
of predicates over states. The predicates Reduces and Stuck hold when
a state can reduce to another one and when no reductions are allowed, respectively.

StateProp : Set$_1$
StateProp = State $\rightarrow$ Set

_$\sim>^*$_ : Rel State _
_$\sim>^*$_ = Star _$\sim>$_

Reduces : StateProp
Reduces S = Satisfiable (S $\sim>$_)

Stuck : StateProp
Stuck S = $\neg$ (Reduces S)

A run is a maximal sequence of states
S $\sim>$ S$_1$ $\sim>$ S$_2$ $\sim>$ $\dots$, that is a
sequence of reductions that is either infinite or it ends with a
stuck state.

data Run (S : State) : Set
record $\infty$Run (S : State) : Set where
field force : Run S

data Run S where
stop : (stuck : Stuck S) $\rightarrow$ Run S
_::_ : $\forall$S' (red : S $\sim>$ S') ($\rho$ : $\infty$Run S') $\rightarrow$ Run S

RunProp : Set$_1$
RunProp = $\forall$S $\rightarrow$ Run S $\rightarrow$ Set

Note that runs are defined using a coinductive record.
RunProp identifies predicates over runs.
Now we model the fact that each property of states induces a corresponding property of
runs in which there is a state that satisfies such property.
A run is finite if it contains a stuck state.

data Eventually (P : StateProp) : RunProp where
here : $\forall$S $\rho$ : Run S (proof : P S) $\rightarrow$ Eventually P $\rho$
next : $\forall$S S' (red : S $\sim>$ S') $\rho$ : $\infty$Run S'
(ev : Eventually P ($\rho$ .force)) $\rightarrow$ Eventually P (red :: $\rho$)

Finite : RunProp
Finite = Eventually Stuck

A fairness assumption is a proposition over runs such that every
partial run S $\sim>^*$ S' can be extended to a fair run. This
condition is called feasibility or machine closure (see <Ref>).

record FairnessAssumption : Set$_1$ where
Fair : RunProp
feasible : $\forall$S S' (reds : S $\sim>^*$ S') $\rightarrow$
$\Sigma$[ $\rho$ $\in$ Run S' ] Fair (reds ++ $\rho$)

StuckFairness : FairnessAssumption
StuckFairness = record  Fair = Fair' ; feasible = feasible'
Fair' : RunProp
Fair' = Eventually (Stuck $\cup$ NonTerminating)

where ++ is used to concatenate runs and StuckFairness
denotes our fairness assumption (see <Ref>). For the sake of
clarity we omit the definition of feasible'.
We recall that a run is fair if it contains finitely many weakly terminating
states. This means that the run is either finite or divergent.
Now we can define fair termination (see <Ref>).
We recall that a state S is fairly terminating if the fair runs of S are finite.

WeaklyTerminating : StateProp
WeaklyTerminating S = $\Sigma$[ $\rho$ $\in$ Run S ] Finite $\rho$

FairlyTerminating : FairnessAssumption $\rightarrow$ StateProp
FairlyTerminating $\phi$ S = $\forall$$\rho$ : Run S $\rightarrow$ Fair $\phi$ $\rho$ $\rightarrow$ Finite $\rho$

Specification : StateProp
Specification S = $\forall$S' $\rightarrow$ S $\sim>^*$ S' $\rightarrow$ WeaklyTerminating S'

Specification is the alternative characterization of fair termination that
does not use fair runs. A state S satisfies the specification if
any S' that is reachable from S is weakly terminating.
A state is weakly terminating if it has a finite run.
Now we can state <Ref> (proofs are omitted).
In particular, we prove that the specification is a necessary condition for fair
termination, regardless of the fairness assumption being made and that
the specification is a sufficient condition for the notion of
fair termination induced by our assumption.

ft$\rightarrow$spec : ($\phi$ : FairnessAssumption) $\rightarrow$ $\forall$S $\rightarrow$
FairlyTerminating $\phi$ S $\rightarrow$ Specification S

spec$\rightarrow$ft : $\forall$S $\rightarrow$
Specification S $\rightarrow$ FairlyTerminating StuckFairness S

At last, as a consequence we can prove that our assumption is the fairness assumption that
induces the largest family of fairly terminating states.

ft$\rightarrow$ft : ($\phi$ : FairnessAssumption) $\rightarrow$
$\forall$S $\rightarrow$ FairlyTerminating $\phi$ S $\rightarrow$
FairlyTerminating StuckFairness S
ft$\rightarrow$ft $\phi$ = spec$\rightarrow$ft $\circ$ ft$\rightarrow$spec $\phi$

§ SESSION TYPES

As noted in <Ref>, we rely on a different definition of (binary) session types
with respect to that presented in <Ref>.
Although such choice has been originally motivated by the fact that we tried to simplify
as much as possible the Agda mechanization of the properties (<Ref>),
it also has the capability of encoding dependent session types, that is,
types that depend on previously exchanged messages. We give more
details later. We first introduce the new formulation of (binary) session types
and then we detail the technical aspects of their formalization.

§.§ Session Types: An Alternative Formulation

§.§ Agda Mechanization of Types

§.§ Agda Mechanization of LTS

§ FAIR TERMINATION

In this section we characterize fair termination of a session type
according to its general formulation in <Ref>.
We say that a session type is fairly terminating if it preserves the possibility
of reaching $\Win$ or $\End[\In]$ along all of its transitions that do not lead to
$\TNil$.  Fair termination of $S$ does not necessarily imply that there exists an
upper bound to the length of communications that follow the protocol $S$, but it
guarantees the absence of “infinite loops” whereby the communication is forced
to continue forever.

§.§ Definition

§.§ Agda Formalization

§ FAIR COMPLIANCE

In this section we define and characterize two compliance relations for
session types, which formalize the “successful” interaction between a client
and a server connected by a session. The notion of “successful interaction”
that we consider is biased towards client satisfaction, but see
<Ref> for a discussion about alternative notions.

§.§ Definition

§.§ Agda Formalization

§ FAIR SUBTYPING

The notions of compliance given in <Ref> induce
corresponding semantic notions of subtyping that can be used to define a safe
substitution principle for session types [Liskov and Wing, 1994]. Intuitively, $\S$
is a subtype of $\T$ if any client that successfully interacts with $\S$ does so
with $\T$ as well.
The reader may look at <Ref> for more details about fair subtyping.

§.§ Definition

§.§ Agda Formalization

§.§ On the Corule

§ CORRECTNESS OF FAIR COMPLIANCE

In this section we detail the mechanized correctness proof of fair compliance
(see point 2. of <Ref>).
As usual, correctness is expressed in terms of soundness and completeness
of _$\compliance{}{}$_ with respect to some specification.
Such specification is defined in <Ref>.
Before looking at such proofs, we formalize <Ref>.
To formalize fair compliance, we define a Success predicate that
characterizes those configurations $\session{R}{S}$ in which the client has succeeded
($R = \Win$) and the server has not failed ($S \neq \TNil$).

data Success : Session $\rightarrow$ Set where
success : $\forall$R S $\rightarrow$ Win R $\rightarrow$ Defined S $\rightarrow$ Success (R , S)

We can weaken Success to MaySucceed,
to characterize those configurations that can be extended so as to become successful ones.
For this purpose we make use of the Satisfiable predicate and of the
intersection $\cap$ of two sets from Agda's standard library.

MaySucceed : Session $\rightarrow$ Set
MaySucceed Se =
Relation.Unary.Satisfiable (Reductions Se $\cap$ Success)

In words, Se may succeed if there exists Se'
such that Se $\wred$ Se' and Se' is a successful configuration.
We can now formulate fair compliance as the property of those sessions that may succeed
no matter how they reduce (see <Ref>). This is the specification against
which we prove soundness and completeness of the for fair compliance (<Ref>).

FCompS : Session $\rightarrow$ Set
FCompS Se = $\forall$Se' $\rightarrow$ Reductions Se Se' $\rightarrow$ MaySucceed Se'

As we did in <Ref>, assume that we want to instaciate Specification
from <Ref> by using Session (see <Ref>)
as set of states and Reduction (see <Ref>) as transition system.
Such instance of Specification would not be equivalent to FCompS as fari compliance
corresponds to a successful form of fair termination.
In order to make them equivalent we would need to parametrize WeaklyTerminating on a predicate
that the reducts have to satisfy. In this case we would say that a state is weakly terminating
if it reduces to another one that is in normal form and that satisfies the input predicate.

§.§ Soundness

§.§ Completeness

§ RELATED WORK

We have shown that generalized inference systems are an effective
framework for defining sound and complete proof systems of (some)
combined safety and liveness properties of (dependent) session types
(<Ref>), as well as of a liveness-preserving
subtyping relation (<Ref>).

Properties of Session Types.
We think that this achievement is more than a coincidence.  One of
the fundamental results in model checking states that every property
can be expressed as the conjunction of a safety property and a
property [Alpern and Schneider, 1985, Alpern and Schneider, 1987, Baier and Katoen, 2008].
The connections between safety and liveness on one side and
coinduction and induction on the other make appropriate for
characterizing combined safety and liveness properties.

[Murgia, 2019] studies a wide range of compliance relations
for processes and session types, showing that many of them are fixed
points of a functional operator, but not necessarily the least or
the greatest ones. In particular, he shows that
progress compliance, which is akin to our compliance (<Ref>), is
a greatest fixed point and that should-testing compliance,
which is akin to our fair compliance (<Ref>), is an
intermediate fixed point. These results are consistent with

Dependent Session Types.
The first theories of dependent session types are those of
[Toninho et al., 2011] and [Griffith and Gunter, 2013]. These
works augment session types with binders, thus allowing for the
specification of message predicates.

[Toninho and Yoshida, 2018] present a full calculus combining functions
and processes in which the structure of both types and processes may
depend on the content of messages.

[Thiemann and Vasconcelos, 2020] propose a full model of functions and
processes enabling a simplified form of dependency whereby the
structure of types and processes may depend on labels and possibly
natural numbers. They introduce a conditional context extension
operator that prevents dependencies on linear values.

[Zhou, 2019] describes the theory and implementation of a
refinement session type system where the type of messages can be
refined by predicates that specify their properties and

Formalizations of Session Type Systems.

[Thiemann, 2019] gives the first mechanized proof of a calculus of
functions and sessions. His type system distinguishes between types
and session types, but only non-dependent pairs are considered.

[de Muijnck-Hughes et al., 2019] describe an Idris EDSL where
dependent types enable reasoning on value dependencies between
exchanged messages.

[Zalakain and Dardha, 2020] give another Agda formalization of the
linear $\pi$-calculus. They focus exclusively on the process layer
and only consider channel types, using typing with
leftovers [Allais, 2017].

[Rouvoet et al., 2020] describe a technique inspired by separation
logic to specify and verify in Agda interpreters using linear
resources. Among the case studies they discuss is a linearly-typed
lambda calculus with primitives for session communications.

CHAPTER: POSTLUDIUM

Let us briefly summarize the two main contents of this thesis.
First, we introduced fair termination as a desirable property in
systems  based on communication as it entails many well known properties
that are studied in the literature.
However, providing a type system for enforcing fair termination is not straightforward
as there exist some peculiar scenarios in which the liveness is compromised.
Then, due to the increasing interest of research communities in proof assistants we
decided to focus on some mechanization aspects. Notably, generalized inference
systems have been a transversal topic throughout the thesis as most of the time we relied on them
for characterizing the definitions that we needed.

Type Systems
On the one hand, in <Ref> we presented a type system for
binary/multiparty sessions which involved fair subtyping. Then we showed
that fair subtyping must be used carefully, that is, finitely many times when it has a strictly
positive weight. The main advantage of the type systems under analysis is that
they allow for compositional reasoning.
On the other hand, in <Ref> we presented a linear logic inspired type system for
the linear $\pi$-calculus. In this case there is no subtyping relation. A peculiar
aspect was that we could type both a fair and an unfair process (see <Ref>)
by using the same type/formula. Differently with respect to the type systems in
<Ref>, the enforcement of fair termination
is based on a global validity condition.
At last, we showed that the type systems cannot be compared which leads to interesting
research directions.
Apart from the technique being used for developing the type systems, we hope
that the reader has been convinced that fair termination is a fundamental
property for communication-based calculi.

Agda Mechanizations
In <Ref> we introduce a library for supporting
generalized inference systems in Agda. Differently, to the built-in techniques,
the library allows to provide modular
definitions that can be composed without duplicating notions.
We then took advantage of such library for characterizing
the properties of session types in <Ref>.
The main aim was to show that well known properties
could be turned into fair ones by adding corules and without changing
the main inference systems (see <Ref>).
The application of foundational aspects to session types tried to provide
a useful guideline for those researchers involved in the formalization of
session type based calculi. Indeed, we also relied on a peculiar definition
of session types that aims at simplifying the definition of the predicates on them.
We hope to have provided some helpful suggestions for realizing the dream according
to which one day all the proofs will be certified.

§ FUTURE WORK

We conclude the thesis by inspecting some possible research directions that we can
take in the future. We are grateful to all the anonymous reviewers of the articles
that we have submitted during these years as they suggested many interesting
topics that we mention in this section.

Fair Termination of Sessions
An open question that may have a relevant practical impact is whether the
type system in <Ref> remain sound
in a setting where communications are
asynchronous. We expect the answer to be positive, as is the case for
other synchronous multiparty session types systems [Scalas and Yoshida, 2019], but
we have not worked out the details yet.
Then, a natural development of these type systems is their application to a
real programming environment. We envision two approaches that can be followed to
this aim. A bottom-up approach may apply our static analysis technique to a
program (in our process calculus) that is extracted from actual code and that
captures the code's communication semantics. We expect that suitable annotations
may be necessary to identify those branching parts of the code that represent
non-deterministic choices in the program. Most typically, these branches will
correspond to finite loops or to queries made to the human user of the program
that have several different continuations. A top-down approach may provide
programmers with a generative tool that, starting from a global
specification in the form of a global type [Honda et al., 2016],
produces template code that is “well-typed by design” and that the programmer
subsequently instantiates to a specific application.
Scribble [Yoshida et al., 2013, Ancona et al., 2016] is an example of such a tool.
Interestingly, the usual notion of global type projectability is not sufficient
to entail that the session map resulting from a projection is coherent. However,
coherence would be guaranteed by requiring that the projected global type is
fairly terminating.

Finally, we plan to investigate the adaptation of the type system for ensuring
the fair termination in the popular actor-based model. This is a drastically
different setting in which the order of messages is not as controllable as in
the case of sessions. As a consequence, type based analyses require radically
different formalisms such as mailbox types [de'Liguoro and Padovani, 2018], for which the
study of fair subtyping and of type systems enforcing fair termination is

Validity in
One drawback of the type system proposed in <Ref> is that establishing whether a
quasi-typed process is also well typed requires a global check on the whole
typing derivation. This does not happen in the type systems for sessions
in <Ref>.
The need for a global check seems to arise commonly in infinitary proof
systems [Dax et al., 2006, Doumane, 2017, Baelde et al., 2016, Baelde et al., 2022],
so an obvious aspect to investigate is whether the analysis can be localized. A
possible source of inspiration for devising a local type system for might
come from the work of [Derakhshan and Pfenning, 2019]. They
propose a compositional technique for dealing with infinitary typing derivations
in a session calculus, although their type system is limited to the additive
fragment of linear logic.

Fair Subtyping and Linear Logic
In <Ref> we showed that the type systems in <Ref>
and the one in <Ref> cannot be compared.
In particular, <Ref> points out a fundamental difference between the two
approaches, that is, the presence or absence of fair subtyping.
Given the rich
literature exploring the connections between linear logic and session types,
and its type system might provide the right framework for investigating
the logical foundations of fair subtyping.

Inference Systems in Agda
For future work we plan to extend the library that we
presented in <Ref> in several directions.
The first one is to support other interpretations of inference systems,
such as the regular one [Dagnino, 2020], which is basically
coinductive but allows only proof trees with finitely many distinct subtrees.
To this end, useful starting points are works on regular terms and streams
[Spadotti, 2016, Uustalu and Veltri, 2017] and on finite sets [Firsov and Uustalu, 2015] in dependent type theories.
The challenging part is the finiteness constraint, which is not trivial in a type-theoretic setting.
A second direction is to implement other proof techniques for (flexible) coinduction,
as parametrized coinduction [Hur et al., 2013] and up-to techniques [Pous, 2016, Danielsson, 2018].
Finally, another direction could be the development of a full framework for composition
of inference systems, along  the lines of seminal work on module systems [Bracha, 1992].
On the more practical side, a further development is to transform the methodology in
an automatic translation. That is, a user should be allowed to write an inference system
(with corules) in a natural syntax, and the corresponding Agda types should be
generated automatically, either by  an external tool, or, more interestingly,
using reflection, recently added in Agda.

[Abel, 2012]
Andreas Abel.
Type-based termination, inflationary fixed-points, and mixed
inductive-coinductive types.
In Dale Miller and Zoltán Ésik, editors,
Proceedings 8th Workshop on Fixed Points in Computer Science, FICS
2012, volume 77 of EPTCS, pages 1–11, 2012.

[Abel and Pientka, 2016]
Andreas Abel and Brigitte Pientka.
Well-founded recursion with copatterns and sized types.
Journal of Functional Programming, 26:0 e2, 2016.

[Abel et al., 2013]
Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer.
Copatterns: programming infinite structures by observations.
In Roberto Giacobazzi and Radhia Cousot, editors, The 40th
Annual ACM Symposium on Principles of Programming Languages, POPL'13,
pages 27–38. ACM, 2013.

[Abel et al., 2017]
Andreas Abel, Andrea Vezzosi, and Théo Winterhalter.
Normalization by evaluation for sized dependent types.
Proceedings of ACM on Programming Languages, 10
(ICFP):0 33:1–33:30, 2017.

[Abramsky, 1994]
Samson Abramsky.
Proofs as processes.
Theor. Comput. Sci., 1350 (1):0 5–9, 1994.

[Abramsky et al., 1996]
Samson Abramsky, Simon J. Gay, and Rajagopal Nagarajan.
Interaction categories and the foundations of typed concurrent
In Manfred Broy, editor, Proceedings of the NATO Advanced
Study Institute on Deductive Program Design, Marktoberdorf, Germany, pages
35–113, 1996.

[Aczel, 1977]
Peter Aczel.
An introduction to inductive definitions.
In Jon Barwise, editor, Handbook of Mathematical Logic,
volume 90 of Studies in Logic and the Foundations of Mathematics,
pages 739 – 782. Elsevier, 1977.

[Allais, 2017]
Guillaume Allais.
Typing with leftovers - A mechanization of intuitionistic
multiplicative-additive linear logic.
In Andreas Abel, Fredrik Nordvall Forsberg, and Ambrus Kaposi,
editors, 23rd International Conference on Types for Proofs and
Programs, TYPES 2017, May 29-June 1, 2017, Budapest, Hungary, volume 104
of LIPIcs, pages 1:1–1:22. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2017.

[Alpern and Schneider, 1985]
Bowen Alpern and Fred B. Schneider.
Defining liveness.
Inf. Process. Lett., 210 (4):0 181–185, 1985.

[Alpern and Schneider, 1987]
Bowen Alpern and Fred B. Schneider.
Recognizing safety and liveness.
Distributed Comput., 20 (3):0 117–126,

[Alpern and Schneider, 1987]
Bowen Alpern and Fred B. Schneider.
Recognizing safety and liveness.
Distributed Comput., 20 (3):0 117–126,

[Altenkirch et al., 2015]
Thorsten Altenkirch, Neil Ghani, Peter G. Hancock, Conor McBride, and Peter
Indexed containers.
Journal of Functional Programming, 25, 2015.

[Ancona et al., 2016]
Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna,
Pierre-Malo Deniélou, Simon J. Gay, Nils Gesbert, Elena Giachino,
Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi,
Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T.
Vasconcelos, and Nobuko Yoshida.
Behavioral types in programming languages.
Found. Trends Program. Lang., 30 (2-3):0
95–230, 2016.

[Ancona et al., 2017]
Davide Ancona, Francesco Dagnino, and Elena Zucca.
Reasoning on divergent computations with coaxioms.
Proceedings of ACM on Programming Languages, 10
(OOPSLA):0 81:1–81:26, 2017a.

[Ancona et al., 2017]
Davide Ancona, Francesco Dagnino, and Elena Zucca.
Generalizing inference systems by coaxioms.
In Hongseok Yang, editor, Programming Languages and Systems -
26th European Symposium on Programming, ESOP 2017, Held as Part of the
European Joint Conferences on Theory and Practice of Software, ETAPS 2017,
Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10201 of
Lecture Notes in Computer Science, pages 29–55. Springer,

[Ancona et al., 2018]
Davide Ancona, Francesco Dagnino, and Elena Zucca.
Modeling infinite behaviour by corules.
In Todd D. Millstein, editor, 32nd European Conference on
Object-Oriented Programming, ECOOP 2018, volume 109 of LIPIcs,
pages 21:1–21:31, Dagstuhl, 2018. Schloss Dagstuhl - Leibniz-Zentrum fuer

[Ancona et al., 2020]
Davide Ancona, Francesco Dagnino, Jurriaan Rot, and Elena Zucca.
A big step from finite to infinite computations.
Science of Computer Programming, 197:0 102492, 2020.
ISSN 0167-6423.

[Apt et al., 1987]
Krzysztof R. Apt, Nissim Francez, and Shmuel Katz.
Appraising fairness in languages for distributed programming.
In Conference Record of the Fourteenth Annual ACM Symposium
on Principles of Programming Languages, Munich, Germany, January 21-23,
1987, pages 189–198. ACM Press, 1987.

[Baelde et al., 2016]
David Baelde, Amina Doumane, and Alexis Saurin.
Infinitary proof theory: the multiplicative additive case.
In Jean-Marc Talbot and Laurent Regnier, editors, 25th
EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 -
September 1, 2016, Marseille, France, volume 62 of LIPIcs, pages
42:1–42:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.

[Baelde et al., 2022]
David Baelde, Amina Doumane, Denis Kuperberg, and Alexis Saurin.
Bouncing threads for circular and non-wellfounded proofs.
In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic
in Computer Science, LICS, 2022, 2022.
URL <https://arxiv.org/abs/2005.08257>.

[Baier and Katoen, 2008]
Christel Baier and Joost-Pieter Katoen.
Principles of model checking.
MIT Press, 2008.
ISBN 978-0-262-02649-9.

[Bellin and Scott, 1994]
Gianluigi Bellin and Philip J. Scott.
On the pi-calculus and linear logic.
Theor. Comput. Sci., 1350 (1):0 11–65, 1994.

[Bernardi and Hennessy, 2016]
Giovanni Bernardi and Matthew Hennessy.
Using higher-order contracts to model session types.
Log. Methods Comput. Sci., 120 (2), 2016.

[Bracha, 1992]
G. Bracha.
The Programming Language JIGSAW: Mixins, Modularity and
Multiple Inheritance.
PhD thesis, Department of Comp. Sci., Univ. of Utah, 1992.

[Bradfield and Stirling, 2007]
Julian C. Bradfield and Colin Stirling.
Modal mu-calculi.
In Patrick Blackburn, J. F. A. K. van Benthem, and Frank Wolter,
editors, Handbook of Modal Logic, volume 3 of Studies in logic
and practical reasoning, pages 721–756. North-Holland, 2007.

[Bravetti et al., 2021]
Mario Bravetti, Julien Lange, and Gianluigi Zavattaro.
Fair refinement for asynchronous session types.
In Stefan Kiefer and Christine Tasson, editors, Foundations of
Software Science and Computation Structures - 24th International Conference,
FOSSACS 2021, Held as Part of the European Joint Conferences on Theory and
Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 -
April 1, 2021, Proceedings, volume 12650 of Lecture Notes in Computer
Science, pages 144–163. Springer, 2021.

[Caires et al., 2016]
Luís Caires, Frank Pfenning, and Bernardo Toninho.
Linear logic propositions as session types.
Math. Struct. Comput. Sci., 260 (3):0
367–423, 2016.

[Carbone and Debois, 2010]
Marco Carbone and Søren Debois.
A graphical approach to progress for structured communication in web
In Simon Bliudze, Roberto Bruni, Davide Grohmann, and Alexandra
Silva, editors, Proceedings Third Interaction and Concurrency
Experience: Guaranteed Interaction, ICE 2010, Amsterdam, The Netherlands,
10th of June 2010, volume 38 of EPTCS, pages 13–27, 2010.
URL <https://doi.org/10.4204/EPTCS.38.4>.

[Carbone et al., 2014]
Marco Carbone, Ornela Dardha, and Fabrizio Montesi.
Progress as compositional lock-freedom.
In Eva Kühn and Rosario Pugliese, editors, Coordination
Models and Languages - 16th IFIP WG 6.1 International Conference,
COORDINATION 2014, Held as Part of the 9th International Federated
Conferences on Distributed Computing Techniques, DisCoTec 2014, Berlin,
Germany, June 3-5, 2014, Proceedings, volume 8459 of Lecture Notes in
Computer Science, pages 49–64. Springer, 2014.
URL <https://doi.org/10.1007/978-3-662-43376-8_4>.

[Carbone et al., 2016]
Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Schürmann, and
Philip Wadler.
Coherence generalises duality: A logical explanation of multiparty
session types.
In Josée Desharnais and Radha Jagadeesan, editors, 27th
International Conference on Concurrency Theory, CONCUR 2016, August 23-26,
2016, Québec City, Canada, volume 59 of LIPIcs, pages
33:1–33:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.

[Carbone et al., 2017]
Marco Carbone, Fabrizio Montesi, Carsten Schürmann, and Nobuko Yoshida.
Multiparty session types as coherence proofs.
Acta Informatica, 540 (3):0 243–269, 2017.

[Castagna et al., 2009]
Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, Elena Giachino, and Luca
Foundations of session types.
In António Porto and Francisco Javier López-Fraguas,
editors, Proceedings of the 11th International ACM SIGPLAN
Conference on Principles and Practice of Declarative Programming, September
7-9, 2009, Coimbra, Portugal, pages 219–230. ACM, 2009.

[Ciccone, 2020]
Luca Ciccone.
Flexible coinduction in agda.
Master's thesis, DIBRIS, Università di Genova, Italy, 2020.
URL <https://arxiv.org/abs/2002.06047>.

[Ciccone and Padovani, 2020]
Luca Ciccone and Luca Padovani.
A dependently typed linear \(\pi\)-calculus in agda.
In PPDP'20: 22nd International Symposium on Principles and
Practice of Declarative Programming, Bologna, Italy, 9-10 September, 2020,
pages 8:1–8:14. ACM, 2020.

[Ciccone and Padovani, 2021]
Luca Ciccone and Luca Padovani.
Inference Systems with Corules for Fair Subtyping and Liveness
Properties of Binary Session Types.
In Nikhil Bansal, Emanuela Merelli, and James Worrell, editors,
Proceedings of the 48th International Colloquium on
Automata, Languages, and Programming (ICALP'21), volume 198 of
LIPIcs, pages 125:1–125:16, Dagstuhl, Germany, 2021a.
Schloss Dagstuhl–Leibniz-Zentrum für Informatik.

[Ciccone and Padovani, 2021]
Luca Ciccone and Luca Padovani.
GitHub repository, 2021b.
URL <https://github.com/boystrange/FairCheck>.

[Ciccone and Padovani, 2021]
Luca Ciccone and Luca Padovani.
GitHub repository, 2021c.
URL <https://github.com/boystrange/FairSubtypingAgda>.

[Ciccone and Padovani, 2022]
Luca Ciccone and Luca Padovani.
Inference systems with corules for combined safety and liveness
properties of binary session types.
Log. Methods Comput. Sci., 180 (3),
URL <https://doi.org/10.46298/lmcs-18(3:27)2022>.

[Ciccone and Padovani, 2022]
Luca Ciccone and Luca Padovani.
An infinitary proof theory of linear logic ensuring fair termination
in the linear \(\pi\)-calculus.
In Bartek Klin, Slawomir Lasota, and Anca Muscholl, editors,
33rd International Conference on Concurrency Theory, CONCUR 2022,
September 12-16, 2022, Warsaw, Poland, volume 243 of LIPIcs, pages
36:1–36:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
URL <https://doi.org/10.4230/LIPIcs.CONCUR.2022.36>.

[Ciccone and Padovani, 2022]
Luca Ciccone and Luca Padovani.
Fair termination of binary sessions.
Proc. ACM Program. Lang., 60 (POPL):0
1–30, 2022c.
URL <https://doi.org/10.1145/3498666>.

[Ciccone et al., 2021]
Luca Ciccone, Francesco Dagnino, and Elena Zucca.
Flexible coinduction in agda.
In Liron Cohen and Cezary Kaliszyk, editors, 12th International
Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1,
2021, Rome, Italy (Virtual Conference), volume 193 of LIPIcs, pages
13:1–13:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,

[Ciccone et al., 2021]
Luca Ciccone, Francesco Dagnino, and Elena Zucca.
GitHub repository, 2021b.
URL <https://lcicc.github.io/inference-systems-agda/>.

[Ciccone et al., 2022]
Luca Ciccone, Francesco Dagnino, and Luca Padovani.
Fair termination of multiparty sessions.
In Karim Ali and Jan Vitek, editors, 36th European Conference
on Object-Oriented Programming, ECOOP 2022, June 6-10, 2022, Berlin,
Germany, volume 222 of LIPIcs, pages 26:1–26:26. Schloss Dagstuhl -
Leibniz-Zentrum für Informatik, 2022.
URL <https://doi.org/10.4230/LIPIcs.ECOOP.2022.26>.

[Courcelle, 1983]
Bruno Courcelle.
Fundamental properties of infinite trees.
Theor. Comput. Sci., 25:0 95–169, 1983.

[Dagnino, 2019]
Francesco Dagnino.
Coaxioms: flexible coinductive definitions by inference systems.
Log. Methods Comput. Sci., 150 (1), 2019.

[Dagnino, 2020]
Francesco Dagnino.
Foundations of regular coinduction.
Technical report, DIBRIS, University of Genova, June 2020.
URL <https://arxiv.org/abs/2006.02887>.
Submitted for journal publication.

[Dagnino, 2021]
Francesco Dagnino.
Foundations of regular coinduction.
Logical Methods in Computer Science, 17:0 2:1–2:29,
URL <https://lmcs.episciences.org/8539>.

[Danielsson, 2018]
Nils Anders Danielsson.
Up-to techniques using sized types.
Proceedings of ACM on Programming Languages, 20
(POPL):0 43:1–43:28, 2018.

[Dardha et al., 2017]
Ornela Dardha, Elena Giachino, and Davide Sangiorgi.
Session types revisited.
Inf. Comput., 256:0 253–286, 2017.

[Dax et al., 2006]
Christian Dax, Martin Hofmann, and Martin Lange.
A proof system for the linear time \(\mathrm{\mu}\)-calculus.
In S. Arun-Kumar and Naveen Garg, editors, FSTTCS 2006:
Foundations of Software Technology and Theoretical Computer Science, 26th
International Conference, Kolkata, India, December 13-15, 2006, Proceedings,
volume 4337 of Lecture Notes in Computer Science, pages 273–284.
Springer, 2006.

[de Muijnck-Hughes et al., 2019]
Jan de Muijnck-Hughes, Edwin Brady, and Wim Vanderbauwhede.
Value-dependent session design in a dependently typed language.
In Francisco Martins and Dominic Orchard, editors, Proceedings
Programming Language Approaches to Concurrency- and Communication-cEntric
Software, PLACES@ETAPS 2019, Prague, Czech Republic, 7th April 2019, volume
291 of EPTCS, pages 47–59. Open Publishing Association, 2019.

[de'Liguoro and Padovani, 2018]
Ugo de'Liguoro and Luca Padovani.
Mailbox types for unordered interactions.
In Todd D. Millstein, editor, 32nd European Conference on
Object-Oriented Programming, ECOOP 2018, July 16-21, 2018, Amsterdam, The
Netherlands, volume 109 of LIPIcs, pages 15:1–15:28. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2018.

[Derakhshan, 2021]
Farzaneh Derakhshan.
Session-Typed Recursive Processes and Circular Proofs.
PhD thesis, Carnegie Mellon University, 2021.

[Derakhshan and Pfenning, 2019]
Farzaneh Derakhshan and Frank Pfenning.
Circular proofs as session-typed processes: A local validity
CoRR, abs/1908.01909, 2019.
URL <http://arxiv.org/abs/1908.01909>.

[DeYoung et al., 2012]
Henry DeYoung, Luís Caires, Frank Pfenning, and Bernardo Toninho.
Cut reduction in linear logic as asynchronous session-typed
In Patrick Cégielski and Arnaud Durand, editors, Computer
Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference
of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France,
volume 16 of LIPIcs, pages 228–242. Schloss Dagstuhl -
Leibniz-Zentrum für Informatik, 2012.

[Doumane, 2017]
Amina Doumane.
On the infinitary proof theory of logics with fixed points.
(Théorie de la démonstration infinitaire pour les logiques
à points fixes).
PhD thesis, Paris Diderot University, France, 2017.
URL <https://tel.archives-ouvertes.fr/tel-01676953>.

[Firsov and Uustalu, 2015]
Denis Firsov and Tarmo Uustalu.
Dependently typed programming with finite sets.
In Patrick Bahr and Sebastian Erdweg, editors, Proceedings of
the 11th ACM Workshop on Generic Programming, WGP@ICFP 2015, pages 33–44.
ACM, 2015.

[Francez, 1986]
Nissim Francez.
Texts and Monographs in Computer Science. Springer, 1986.
ISBN 978-3-540-96235-9.

[Gardner et al., 2007]
Philippa Gardner, Cosimo Laneve, and Lucian Wischik.
Linear forwarders.
Inf. Comput., 2050 (10):0 1526–1550, 2007.

[Gay, 2016]
Simon J. Gay.
Subtyping supports safe session substitution.
In Sam Lindley, Conor McBride, Philip W. Trinder, and Donald
Sannella, editors, A List of Successes That Can Change the World -
Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday,
volume 9600 of Lecture Notes in Computer Science, pages 95–108.
Springer, 2016.

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

[Gay and Vasconcelos, 2010]
Simon J. Gay and Vasco Thudichum Vasconcelos.
Linear type theory for asynchronous session types.
J. Funct. Program., 200 (1):0 19–50, 2010.

[Griffith and Gunter, 2013]
Dennis Griffith and Elsa L. Gunter.
Liquidpi: Inferrable dependent session types.
In Guillaume Brat, Neha Rungta, and Arnaud Venet, editors,
NASA Formal Methods, 5th International Symposium, NFM 2013, Moffett
Field, CA, USA, May 14-16, 2013. Proceedings, volume 7871 of Lecture
Notes in Computer Science, pages 185–197. Springer, 2013.

[Honda, 1993]
Kohei Honda.
Types for dyadic interaction.
In Eike Best, editor, CONCUR '93, 4th International
Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993,
Proceedings, volume 715 of Lecture Notes in Computer Science, pages
509–523. Springer, 1993.

[Honda et al., 1998]
Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo.
Language primitives and type discipline for structured
communication-based programming.
In Chris Hankin, editor, Programming Languages and Systems -
ESOP'98, 7th European Symposium on Programming, Held as Part of the European
Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon,
Portugal, March 28 - April 4, 1998, Proceedings, volume 1381 of
Lecture Notes in Computer Science, pages 122–138. Springer, 1998.

[Honda et al., 2008]
Kohei Honda, Nobuko Yoshida, and Marco Carbone.
Multiparty asynchronous session types.
In George C. Necula and Philip Wadler, editors, Proceedings of
the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008,
pages 273–284. ACM, 2008.

[Honda et al., 2016]
Kohei Honda, Nobuko Yoshida, and Marco Carbone.
Multiparty asynchronous session types.
J. ACM, 630 (1):0 9:1–9:67, 2016.

[Hur et al., 2013]
Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis.
The power of parameterization in coinductive proof.
In Roberto Giacobazzi and Radhia Cousot, editors, The 40th
Annual ACM Symposium on Principles of Programming Languages, POPL'13,
pages 193–206. ACM, 2013.

[Hüttel et al., 2016]
Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Luís Caires, Marco
Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani,
António Ravara, Emilio Tuosto, Hugo Torres Vieira, and Gianluigi
Foundations of session types and behavioural contracts.
ACM Comput. Surv., 490 (1):0 3:1–3:36,

[Jacobs et al., 2022]
Jules Jacobs, Stephanie Balzer, and Robbert Krebbers.
Connectivity graphs: a method for proving deadlock freedom based on
separation logic.
Proc. ACM Program. Lang., 60 (POPL):0
1–33, 2022.

[Kobayashi, 2002]
Naoki Kobayashi.
A type system for lock-free processes.
Inf. Comput., 1770 (2):0 122–159,

[Kobayashi, 2002]
Naoki Kobayashi.
Type systems for concurrent programs.
In 10th Anniversary Colloquium of UNU/IIST, LNCS 2757, pages
439–453. Springer, 2002b.
Extended version at
<http://www.kb.ecei.tohoku.ac.jp/ koba/papers/tutorial-type-extended.pdf>.

[Kobayashi, 2006]
Naoki Kobayashi.
A new type system for deadlock-free processes.
In Christel Baier and Holger Hermanns, editors, CONCUR 2006 -
Concurrency Theory, 17th International Conference, CONCUR 2006, Bonn,
Germany, August 27-30, 2006, Proceedings, volume 4137 of Lecture Notes
in Computer Science, pages 233–247. Springer, 2006.

[Kobayashi and Laneve, 2017]
Naoki Kobayashi and Cosimo Laneve.
Deadlock analysis of unbounded process networks.
Inf. Comput., 252:0 48–70, 2017.

[Kobayashi and Sangiorgi, 2010]
Naoki Kobayashi and Davide Sangiorgi.
A hybrid type system for lock-freedom of mobile processes.
ACM Trans. Program. Lang. Syst., 320 (5):0
16:1–16:49, 2010.

[Kobayashi et al., 1999]
Naoki Kobayashi, Benjamin C. Pierce, and David N. Turner.
Linearity and the pi-calculus.
ACM Trans. Program. Lang. Syst., 210 (5):0
914–947, 1999.

[Kokke et al., 2018]
Wen Kokke, Fabrizio Montesi, and Marco Peressotti.
Taking linear logic apart.
In Thomas Ehrhard, Maribel Fernández, Valeria de Paiva, and
Lorenzo Tortora de Falco, editors, Proceedings Joint International
Workshop on Linearity & Trends in Linear Logic and Applications,
Linearity-TLLA@FLoC 2018, Oxford, UK, 7-8 July 2018, volume 292 of
EPTCS, pages 90–103, 2018.

[Kokke et al., 2019]
Wen Kokke, Fabrizio Montesi, and Marco Peressotti.
Better late than never: a fully-abstract semantics for classical
Proc. ACM Program. Lang., 30 (POPL):0
24:1–24:29, 2019.

[Kozen, 1983]
Dexter Kozen.
Results on the propositional mu-calculus.
Theor. Comput. Sci., 27:0 333–354, 1983.

[Lamport, 2000]
Leslie Lamport.
Fairness and hyperfairness.
Distributed Comput., 130 (4):0 239–245, 2000.

[Leroy and Grall, 2009]
Xavier Leroy and Hervé Grall.
Coinductive big-step operational semantics.
Information and Computation, 2070 (2):0
284–304, 2009.

[Lindley and Morris, 2015]
Sam Lindley and J. Garrett Morris.
A semantics for propositions as sessions.
In Jan Vitek, editor, Programming Languages and Systems - 24th
European Symposium on Programming, ESOP 2015, Held as Part of the European
Joint Conferences on Theory and Practice of Software, ETAPS 2015, London,
UK, April 11-18, 2015. Proceedings, volume 9032 of Lecture Notes in
Computer Science, pages 560–584. Springer, 2015.
URL <https://doi.org/10.1007/978-3-662-46669-8_23>.

[Lindley and Morris, 2016]
Sam Lindley and J. Garrett Morris.
Talking bananas: structural recursion for session types.
In Jacques Garrigue, Gabriele Keller, and Eijiro Sumii, editors,
Proceedings of the 21st ACM SIGPLAN International Conference on
Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016,
pages 434–447. ACM, 2016.

[Liskov and Wing, 1994]
Barbara Liskov and Jeannette M. Wing.
A behavioral notion of subtyping.
ACM Trans. Program. Lang. Syst., 160 (6):0
1811–1841, 1994.

[Milner, 1978]
Robin Milner.
A theory of type polymorphism in programming.
J. Comput. Syst. Sci., 170 (3):0 348–375,
URL <https://doi.org/10.1016/0022-0000(78)90014-4>.

[Murgia, 2019]
Maurizio Murgia.
A note on compliance relations and fixed points.
In Massimo Bartoletti, Ludovic Henrio, Anastasia Mavridou, and
Alceste Scalas, editors, Proceedings 12th Interaction and Concurrency
Experience, ICE 2019, Copenhagen, Denmark, 20-21 June 2019, volume 304 of
EPTCS, pages 38–47, 2019.

[Owicki and Lamport, 1982]
Susan S. Owicki and Leslie Lamport.
Proving liveness properties of concurrent programs.
ACM Trans. Program. Lang. Syst., 40 (3):0
455–495, 1982.

[Padovani, 2013]
Luca Padovani.
Fair subtyping for open session types.
In Fedor V. Fomin, Rusins Freivalds, Marta Z. Kwiatkowska, and David
Peleg, editors, Automata, Languages, and Programming - 40th
International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013,
Proceedings, Part II, volume 7966 of Lecture Notes in Computer
Science, pages 373–384. Springer, 2013.

[Padovani, 2014]
Luca Padovani.
Deadlock and lock freedom in the linear \(\pi\)-calculus.
In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting
of the Twenty-Third EACSL Annual Conference on Computer Science Logic
(CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer
Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages
72:1–72:10. ACM, 2014.

[Padovani, 2016]
Luca Padovani.
Fair subtyping for multi-party session types.
Math. Struct. Comput. Sci., 260 (3):0
424–464, 2016.

[Padovani, 2017]
Luca Padovani.
A simple library implementation of binary sessions.
J. Funct. Program., 27:0 e4, 2017.

[Padovani, 2022]
Luca Padovani.
GitHub repository, 2022.
URL <https://github.com/boystrange/FairTermination>.

[Pérez et al., 2012]
Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho.
Linear logical relations for session-based concurrency.
In Helmut Seidl, editor, Programming Languages and Systems -
21st European Symposium on Programming, ESOP 2012, Held as Part of the
European Joint Conferences on Theory and Practice of Software, ETAPS 2012,
Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, volume 7211 of
Lecture Notes in Computer Science, pages 539–558. Springer, 2012.

[Pous, 2016]
Damien Pous.
Coinduction all the way up.
In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors,
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in
Computer Science, LICS'16, pages 307–316. ACM, 2016.

[Qian et al., 2021]
Zesen Qian, G. A. Kavvos, and Lars Birkedal.
Client-server sessions in linear logic.
Proc. ACM Program. Lang., 50 (ICFP):0
1–31, 2021.

[Queille and Sifakis, 1983]
Jean-Pierre Queille and Joseph Sifakis.
Fairness and related properties in transition systems - A temporal
logic to deal with fairness.
Acta Informatica, 19:0 195–220, 1983.

[Rocha and Caires, 2021]
Pedro Rocha and Luís Caires.
Propositions-as-types and shared state.
Proc. ACM Program. Lang., 50 (ICFP):0
1–30, 2021.

[Rouvoet et al., 2020]
Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, and Eelco Visser.
Intrinsically-typed definitional interpreters for linear,
session-typed languages.
In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings
of the 9th ACM SIGPLAN International Conference on Certified Programs and
Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages
284–298. ACM, 2020.

[Sangiorgi, 2011]
Davide Sangiorgi.
Introduction to Bisimulation and Coinduction.
Cambridge University Press, 2011.

[Scalas and Yoshida, 2019]
Alceste Scalas and Nobuko Yoshida.
Less is more: multiparty session types revisited.
Proc. ACM Program. Lang., 30 (POPL):0
30:1–30:29, 2019.

[Scalas et al., 2017]
Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida.
A linear decomposition of multiparty sessions for safe distributed
programming (artifact).
Dagstuhl Artifacts Ser., 30 (2):0 03:1–03:2,

[Spadotti, 2016]
Régis Spadotti.
A mechanized theory of regular trees in dependent type theory.
(Une théorie mécanisée des arbres réguliers en
théorie des types dépendants).
PhD thesis, Paul Sabatier University, Toulouse, France, 2016.
URL <https://tel.archives-ouvertes.fr/tel-01589656>.

[Stirling, 2001]
Colin Stirling.
Modal and Temporal Properties of Processes.
Texts in Computer Science. Springer, 2001.
ISBN 978-1-4419-3153-5.

[The Agda Team, 2022]
The Agda Team.
The Agda Reference Manual, 2022.
URL <http://agda.readthedocs.io/en/latest/index.html>.

[Thiemann, 2019]
Peter Thiemann.
Intrinsically-typed mechanized semantics for session types.
In Ekaterina Komendantskaya, editor, Proceedings of the 21st
International Symposium on Principles and Practice of Programming Languages,
PPDP 2019, Porto, Portugal, October 7-9, 2019, pages 19:1–19:15. ACM,

[Thiemann and Vasconcelos, 2020]
Peter Thiemann and Vasco T. Vasconcelos.
Label-dependent session types.
Proc. ACM Program. Lang., 40 (POPL):0
67:1–67:29, 2020.

[Toninho and Yoshida, 2018]
Bernardo Toninho and Nobuko Yoshida.
Depending on session-typed processes.
In Christel Baier and Ugo Dal Lago, editors, Foundations of
Software Science and Computation Structures - 21st International Conference,
FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and
Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018,
Proceedings, volume 10803 of Lecture Notes in Computer Science, pages
128–145. Springer, 2018.

[Toninho et al., 2011]
Bernardo Toninho, Luís Caires, and Frank Pfenning.
Dependent session types via intuitionistic linear type theory.
In Peter Schneider-Kamp and Michael Hanus, editors,
Proceedings of the 13th International ACM SIGPLAN Conference on
Principles and Practice of Declarative Programming, July 20-22, 2011, Odense,
Denmark, pages 161–172. ACM, 2011.

[Uustalu and Veltri, 2017]
Tarmo Uustalu and Niccolò Veltri.
Finiteness and rational sequences, constructively.
Journal of Functional Programming, 27:0 e13, 2017.

[van Glabbeek and Höfner, 2019]
Rob van Glabbeek and Peter Höfner.
Progress, justness, and fairness.
ACM Comput. Surv., 520 (4):0 69:1–69:38,

[van Glabbeek et al., 2021]
Rob van Glabbeek, Peter Höfner, and Ross Horne.
Assuming just enough fairness to make session types complete for
In 36th Annual ACM/IEEE Symposium on Logic in Computer
Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1–13.
IEEE, 2021.

[Wadler, 2014]
Philip Wadler.
Propositions as sessions.
J. Funct. Program., 240 (2-3):0 384–418,

[Yoshida et al., 2013]
Nobuko Yoshida, Raymond Hu, Rumyana Neykova, and Nicholas Ng.
The scribble protocol language.
In Martín Abadi and Alberto Lluch-Lafuente, editors,
Trustworthy Global Computing - 8th International Symposium, TGC 2013,
Buenos Aires, Argentina, August 30-31, 2013, Revised Selected Papers, volume
8358 of Lecture Notes in Computer Science, pages 22–41. Springer,

[Zalakain and Dardha, 2020]
Uma Zalakain and Ornela Dardha.
Typing the linear pi calculus in Agda, 2020.
URL <https://github.com/umazalakain/typing-linear-pi>.

[Zalakain and Dardha, 2021]
Uma Zalakain and Ornela Dardha.
Co-contextual typing inference for the linear \(\pi\)-calculus in
agda (extended abstract).
Extended abstract at Workshop on Type-Driven Development (TyDe) 2021,

[Zhou, 2019]
Fangyi Zhou.
Refinement session types, 2019.
BSc Dissertation.

CHAPTER: SUPPLEMENT TO CHAPTER 4