Luca Ciccone

UNIVERSITÀ DEGLI STUDI DI TORINO
10 pt

DIPARTIMENTO DI INFORMATICA

10 pt

SCUOLA DI SCIENZE DELLA NATURA

10 pt

Doctoral School in Computer Science - Cycle XXXV

20 pt

Concerto Grosso
6 pt
6 pt
Fair Termination of Sessions

60 pt

20 pt

Luca Ciccone

Prof. Luca Padovani
Prof. Ugo de'Liguoro

Prof. Eugenio Moggi
Prof. Ornela Dardha

\[
\begin{array}{rl}
\text{\textbf{\textit{PhD Coordinator}}:} & \text{Prof. Viviana Patti}
\\
\text{\textbf{\textit{Submitted on}}:} & \text{December 2022}
\end{array}
\]

CHAPTER: GRATIAS VOBIS AGO

§ INSTITUTIONAL

To University of Torino and the entire PhD board
2020 and 2021 have been hard years for everyone. However, UniTo successfully managed to provide
courses and side activities in the best way possible. At the beginning of 2020 TYPES conference should have been
held in Torino but COVID was spreading in Italy. The conference moved to a virtual space.
No one knew it was the first of a long sequence of remote events.
PhD related events have been obviously affected as well.
Nonetheless, courses have been well organized fast in a remote fashion.

To my supervisor Luca Padovani
I skip the COVID part as it would be obvious and I move to mere professional considerations.
As soon as my PhD started Luca and I discussed about the ways in which we could have taken advantage of
the work I did during the master thesis. This way we immediately found the right intersection between by knowledge
and my PhD project and we started working together. I never worked for but with him.
Such an approach led to fast and satisfactory research outcomes. Moreover Luca always shared his connections with other
research groups, at University of Glasgow.
I have been his first PhD student so I hope that these lines will give him a feedback about his supervision.

To University of Genova and Elena Zucca
My master thesis supervisor Elena Zucca agreed with Luca for giving me an office at DIBRIS, UniGe.
This way we could start a fruitful research collaboration.
During last year we managed to publish together a paper at ECOOP that earned the distinguished paper award.
Hence, I'm grateful to both the University of Genova and Elena for allowing me to use such office.

To EuroProofNet, University of Glasgow and Ornela Dardha
After two years of remote human interactions, in-person events started again. During the pandemic I have been in touch with
Ornela Dardha whose research interests were very close to mine. Unfortunately I could not have met her research group.
In the meantime EuroProofNet, a european project aimed at connecting researchers on formal proofs, was born.
Such project gave me the funds for making two visits to Ornela Dardha at University of Glasgow.
I have been welcomed in the best way.

To the reviewers
I'm grateful to Eugenio Moggi and Ornela Dardha for having spent a lot of time
reading this thesis. They provided useful comments and important references.
I hope this work will be useful for their research groups.

§ ...A LITTLE FLATTERY

To my super-visor Luca Padovani
Coming to personal considerations, I am grateful to Luca for many reasons.
In general, as an empathetic person I found his approach of sharing not only his ideas
but also his feelings very inspiring. I learned how to face a variety of situations
thanks to him, from the anxiety in meeting deadlines to the tricks in providing
successful presentations. These skills will be helpful for my career.
Last but not least, I'd like to thank Luca for his support during the pandemic when I had
serious COVID problems in my family; we were writing the ICALP paper and the result has been

To my unofficial supervisor Elena Zucca
I'd like to express my gratitude to Elena for her precious suggestions during the PhD and before
starting it. She put me in touch with Luca Padovani at the end of my master thesis.
Although she was not officially reported as my co-supervisor, she demonstrated a high
involvement in working together as well as with my colleague and friend Francesco Dagnino (UniGe).
As for Luca, I'd like to thank her for her support when I had COVID problems in my family.
When I was working on the ICALP paper with Luca, in the meantime I was writing the ITP one
with Elena and Francesco. Such paper has been accepted and together with the PPDP one it
introduced me to the formal proofs community.

To Ornela Dardha
I had the opportunity of meeting Ornela only last year. She welcomed me in Glasgow
as a friend more than as a professor.
I immediately discovered that it was not just
a special treatment for visitors as she has a very special way of dealing with her research group.

SPLS, 26th October 2022.

Although I'm usually not so keen on those situations in which
colleagues and friends automatically overlap, I'm sure that Ornela's approach
is fantastic both for her students and visitors. The reason behind my opinion is that
Ornela is a very empathetic person and she cares about the mood of others a lot.
For this reason I decided to visit her two more times the same year and I really hope to meet her again
even if I will not be involved in the research world anymore.

That's okay for today. Now you should go to the pub! (cit.)

§ PERSONAL

To my family
This is a special paragraph. I'm usually in trouble when I have to write something
to express my gratitude to my family as putting on paper deep feelings is a very hard task
(and I also have to deal with my eyes filled with tears). What lies behind the usual sentence
for their support and blah blah? I would like to completely change the point of view
and try something new. Obviously, the focus is on my parents Renato Ciccone and Marirosa Gaggero.
Let me start with a consideration: I trust stereotypes and in Genova we are famous as people that
do not want to spend money. My studies were not free of course, so I'm very grateful to my parents
for the sacrifices they made for paying a lot for so many years.
Although I managed to win scolarships different times,
I always used such money for whatever but paying university subscriptions; I was younger and naive.
Furthermore, when I decided to start a PhD, I always asked myself whether such a title would have
been useful for my career outside the academy.
I honestly shared my doubts with my parents. In the end I found
a satisfactory number of job opportunities positively influenced by these three years of research.
At last, the years of PhD, and in particular the last one, made me grow up a lot as a person.
Hence, I hope to have made my parents proud of the results.

To my grandmother Anna (Ciccone) Peruzzi
Things become harder. She is a dresskmaker for children, she loves classical music,
she attends theatres and music associations...more in general, she loves beauty in its essence.
What is a person without any cultural interest?, she always asked.
From her I learned the things to appreciate and study in my free time and that I deepened every day.
I'm grateful to her for her ambitions towards me that I hope to have satisfied.

To my ggf Ruggero Peruzzi

Ruggero Peruzzi after Edmé Bouchardon.

He was born on 19 Novemeber, 1891.
He was an antiquarian in Genova.
My grandmother learned from him the love of beauty.
During a journey he met the painter C. Tafuri and he paid for him an office in
Palazzo della Borsa in Genova.
During WW2 he has been captured by fascists as they wanted the names of
some partisans. He never told such information and fascists started torturing him.
He had only one opportunity to say goodbye to her daughter.
He has been killed by fascists and his body has been found on 18 February 1945
in front of Brignole train station in Genova where you can find his tombstone.

Concerto Grosso?
This last acknowledgment goes to A. Schnittke, A. Schönberg, A. Berg, J. S. Bach, B. Galuppi, A. Pärt
as well as to many other great composers. In particular, Schnittke's music has been the soundtrack of
the last three years. His Concerti Grossi obviously recall baroque music but at the same time they
are progressively cracked and filled with XXth century influences.

CHAPTER: OVERTURE

Sessions are a fundamental notion in message-passing systems. A session is an abstract notion of
communication between parties where each one owns an endpoint.
Session types are types that are assigned to the endpoints and that are used to statically and dynamically
enforce some desired properties of the communications, such as the absence of deadlocks.

Properties of concurrent systems are usually
divided in safety and liveness ones and depending on the class it belongs to, a property is defined
using different (dual) techniques. However, there exist some properties that require to mix both techniques
and the challenges in defining them
are exacerbated in proof assistants (Agda, Coq, $\dots$),
that is, tools that allow users to formally characterize and prove theorems. In particular, we mechanize
the meta-theory of inference systems in Agda.

Among the interesting properties that can be studied in the session-based context, we study
fair termination which is the property of those sessions that can always eventually reach
successful termination under a fairness assumption. Fair termination
implies many desirable and well known properties, such as lock freedom. Moreover, a lock free session
does not imply that other sessions are lock free as well. On the other hand, if we consider a session and
we assume that all the other ones are fairly terminating, we can conclude that the one under analysis is
fairly terminating as well.

CHAPTER: PRAELUDIUM

Nowadays concurrent and distributed systems are ubiquitous in the computer science world.
It is not surprising that there exists a wide research about how to enforce some desired
properties of communications in such systems.

§ A GENTLE INTRODUCTION

The $\pi$-calculus is a process calculus used for modeling concurrent systems and it is based
on channels that are owned by the entities involved in the communication and that are
used to exchange messages.
Session types [Honda, 1993] are a formalism to describe communication protocols.
A session is represented by a channel that connects processes and session types are assigned to them.
They describe how the channels will be used by the processes that own them.
Session types have been originally introduced to model the interaction between two entities
and they have been later generalized to multiparty [Honda et al., 2008].

There exists a broad family of desired properties that one would like to enforce in a communication.
Among them, the most common ones are that messages are exchanged in the right order (protocol fidelity)
or that there are no communication errors (communication safety).

Safety vs Liveness - Fair Termination
In general, properties can be divided in safety (nothing bad ever happens) and
liveness (something good will eventually happen) ones [Owicki and Lamport, 1982].
According to the class to which it belongs, a property is defined using different and dual
techniques: induction for safety and coinduction for liveness.
Actually, there exist some properties that fall in between as they combine safety and
liveness aspects. We can informally describe them using the motto “something good always eventually
happens” and their dual. Hence, such properties are hard to deal with as they mix induction
and coinduction.
In a communication-based scenario, protocol fidelity is a safety property and the eventual termination
of a session is a liveness one.
In this thesis we study fair termination which is the property of those sessions that can always
eventually (successfully) terminate under a fairness assumption. As the reader might guess, fair termination
joins a safety and a liveness part. We investigate such property as it entails many well knows properties
that are studied in the literature.

Fair Subtyping
Subtyping between session types is a fundamental relation in this thesis. It induces
a substitution principle [Liskov and Wing, 1994] which states that a process that uses an
endpoint according to some type can be substituted with another process that uses the
endpoint according to a supertype. Although the principle seems in the wrong direction
it is proved to be equivalent to the right-to-left variant by taking into account endpoints
instead of processes [Gay, 2016].
The original subtyping relation [Gay and Hole, 2005] is studied to preserve the safety properties of
a session but not the livess ones. Indeed an application of the original subtyping can
break the termination property of the involved session.
In this thesis we rely on fair subtyping [Padovani, 2014, Padovani, 2016] which is
a liveness-preserving variant of the subtyping in [Gay and Hole, 2005].

(Generalized) Inference Systems
Inference systems are a widely used framework in computer science for defining predicates by means of (meta) rules.
They support both inductive and coinductive definitions and they have been recently generalized
to deal with those predcates that mix the two approaches [Ancona et al., 2017].
Roughly, an inference system, that is, a set of (meta)rules, is interpreted either
inductively or coinductively. In a generalized inference system the key ingredient
is the addition of (meta)corules and the interpretation is obtained by properly mixing the inductive and
the coinductive one.
Then, inference systems also provide proof principles for proving the correctness of
a definition with respect to a semantic one called specification in a canonical way.
Correctness is usually expressed in terms of soundness and completeness.
The reference principles are induction, coinduction which involve
inductive and coinductive predicates, respectively.
Bounded coinduction is a generalization of coinduction and is used when dealing
with definitions through generalized inference systems.
We will rely on (generalized) inference systems for defining most
of the notions we will introduce.

Proof Assistants
These days there is an increasing interest in theorem provers, that is, tools
that allow users to write proofs by relying on a language that resembles a programming language.
The advantage of using proof assistants is that the proofs are certified (provided that the tool is
itself consistent).
Due to the novelty of the research field, there is a focus in the literature in providing big libraries
with the aim of making the community agree on some design techniques. For example,
when formalizing calculi, De Bruijn indices are usually preferred for dealing with variables.
Many research communities are starting to rely on theorem provers to mechanize existing theories.
The community working on behavioral types is affected by this phenomenon as well.
Moreover, apart from traditional conferences on formal proofs (CPP, ITP), a very first
workshop on Verification of Session Types has been organized in 2020 and 2021.
The main output of such event was the lack of a reference methodology for mechanizing
session-based theories. In this thesis we will refer to the Agda proof assistant [The Agda Team, 2022].
Notably, we refer to theorem provers and proof assistant interchangeably.

Agda [The Agda Team, 2022] is an interactive proof assistant based on intuitionistic logic. The interactivity aspect
is fundamental as the user is guided step-by-step while mechanizing a proof.
The tool can be download for different platforms and comes with only the very basic
definitions, natural numbers. The standard library can be added separately
and it is constantly updated in order to keep the modules consistent with the latest
version of Agda.
Moreover, Agda has built-in support for both inductive and coinductive predicates.
In [Ciccone, 2020] we made an in-depth analysis of all the techniques that users can
follow when mechanizing predicates and we found out that pure (co)inductive
inference system have a natural and intuitive encoding in Agda.
However, for what concerns those predicates defined by generalized inference systems,
there is no support. Indeed, although a generalized inference system can still be
defined, the resulting code becomes hard to understand and it contains many duplicated

§ CONTRIBUTIONS

Can well-typed programs go well?

Developing type systems for enforcing liveness properties of processes is not
an easy task. For example, in the context of this thesis the type systems
of [Kobayashi, 2002, Padovani, 2014] adopt a sophisticated technique for guaranteeing
that all pending actions will be eventually executed. The question we want to answer
is in sharp contrast with the famous Robin Milner's sentence “Well typed programs cannot
go wrong” [Milner, 1978] which points out the fact that type systems are usually made for enforcing
safety aspects.

Fair Termination
We present type systems for enforcing fair termination in three different scenarios.
First, we deal with binary sessions, that is, sessions involving only two
participants. This base case is fundamental to highlight all the technical aspects
and additional properties that the type system must ensure in order to guarantee
fair termination.
Then, we generalize such type system to the multiparty case. Although
many notions can be easily adapted from the binary case, there are some technical
details that are hard to deal with. For what concerns the additional properties that
the type system has to enforce, we can still rely on the binary type system since binary
sessions are the simplest multiparty ones.
At last, we show a type for enforcing fair termination in the linear $\pi$-calculus.
This last part falls in between the previous type systems and those type systems
interpreting session-based calculi in the context of linear logic.
The interesting difference between the type systems for sessions and the one for the $\pi$-calculus
is that in the second there is no notion of fair subtyping.

Can Agda support definitions mixing induction and coinduction?

Can Agda proofs match the pen-and-paper ones?

As we mentioned before, Agda supports purely (co)inductive definitions. Moreover,
a predicate defined using an inference system can be naturally encoded.
On the other hand, when we deal with a predicate that involves both induction and coinduction,
there is no built-in support [Ciccone, 2020].
As a result, we can still mechanize such predicates but
the resulting code contains many duplicated notions and it differs from the definition
given through a generalized inference system.
Another drawback of mechanizing notions in Agda is that the proofs become very hard to
be understood as they differ from the hand written ones since they require many additional
lemmas related to the technicalities of the proof assistant, equalities.
Hence, we first ask whether it is possible to encode generalized inference systems in Agda
in a natural way. Then we ask if we can “hide” all the Agda related technicalities
so that the proofs are shown to the user in a more friendly flavor.

An Agda Library for Inference Systems
(Generalized) inference systems are used throughout the entire thesis.
Since we aimed at mechanizing some results in Agda, we thought about a way for
supporting the framework in the proof assistant. For this sake we present a
library that allows users to formalize inference systems using a syntax that
resembles the one used on paper. Moreover, the library supports the usage of
corules that are not built-in supported (see [Ciccone, 2020] for more details).
Clearly, all the proof principles are encoded as well.
As an important and useful side effect, the codes of the proofs based on the library
resemble the proofs written on paper. We think that this contribution
can be very helpful for the community since closed proofs are usually very hard
to read and understand.

Mechanizing Properties of Session Types
We take advantage of the library we developed to mechanize some notions in the
session types context.
We first mechanize an alternative definition of session types that aims at
simplifying the codes as much as possible. Such characterization has also the
advantage of supporting dependency with respect to previously exchanged messages.
Then we focus on three interesting properties of session types and we characterize them
using generalized inference systems: fair termination of a session type, fair compliance
(successful fair termination) of a binary session and fair subtyping.
We mechanize the three inference system as well as their correctness proofs with
respect to the semantic definitions.
As mentioned before, the community working on session types is increasingly interested
in proof assistants but so far there is a lack of a reference methodology.
We hope that our results and our experience will be used for finding
a guideline on which all the community agrees.

§ STRUCTURE OF THE THESIS

Concerto Grosso
As the title might suggest, the thesis is structured in three parts as the original italian
Concerto Grosso form of baroque music.
Moreover, since binary sessions are the simplest multiparty ones, we will jump between the two
scenarios according to our needs. In general, we will show paradigmatic examples in the binary setting
and we will prove the main notions in the more general multiparty one.
The continuous alternation of communications between two and more participants
resembles again the Concerto Grosso which is based on a dialogue between a small ensemble
and the full orchestra.
The tempo indications at the beginning of each part are consistent with the fast-slow-fast schema
of the concerto grosso and we use them to jokingly indicate that the part that should be read more
carefully is the central one. At last, in order to help the reader we use treble, soprano and bass clefs to
denote texts inside chapters, sections and subsections, respectively.

Part I: Key Notions
There are different notions that we will use throughout <Ref>.
Thus, we decided to dedicate the first part to introduce all the main ingredients of
the thesis.

At the beginning we discuss the usual classification of properties in safety and liveness ones in <Ref>.
Then, in <Ref> we introduce (Generalized) inference systems as a reference framework
and in <Ref> we introduce syntax and semantics of binary and multiparty session types.

We dedicate <Ref> to explain what is fair termination and to express it in a general
setting, that is, considering an arbitrary transition system. Then, we instantiate the property
in the session types context.

At last, in <Ref> we focus on the subtyping relation between session types.
We first introduce the original subtyping relation [Gay and Hole, 2005] and we show why
it can break the liveness properties on the session on which it is applied.
We then introduce fair subtyping as a liveness-preserving refinement of the original relation.
We present fair subtyping in two different flavours; first using a purely coinductive
inference system and then using a generalized inference system.

Part II: Type Systems
This part is dedicated to the study of the three type systems for fair termination
and it is split according to the calculus under analysis.

In <Ref> we present a type system for a calculus with binary sessions.
<Ref> generalizes such type system to the multiparty case.
At last, in <Ref> we show a type system for a $\pi$-calculus that is
based on linear logic.

The three chapters are stuctured similarly.
We first introduce the calculus (and the types) and then we show the typing rules.
We dedicate the rest of each chapter to detail the soundness proofs.
As we mentioned before, in <Ref> we focus on those paradigmatic
examples that point out the additional properties that the type system must enforce.
Since such examples hold in the multiparty setting as well, in <Ref>
we present some more involved processes.

Part III: Agda Mechanizations
This third and last part focuses on the mechanization aspects.

In <Ref> we present the library for supporting in Agda generalized
inference systems. We first mechanize the meta theory of inference systems as well
as the proof principles and then we show some basic examples of usage.
Then in <Ref> we present the definitions through generalized inference
systems of three properties of session types: fair termination of a session type,
fair compliance of a binary session and fair subtyping.
Notably, we mechanize the general notion of fair termination and we
relate it to the semantic definitions of the first two properties.
For each property we show the mechanization of the inference system and
we show how proof principles are used in the correctness proofs.
At last, we detail the proofs of fair compliance.

§ PUBLISHED WORKS

We conclude the introduction by relating the content of the thesis with
the published works of the author.

Fair Termination
<Ref> is a refined version of [Ciccone and Padovani, 2022].
Differently from [Ciccone and Padovani, 2022], here we adopt the new characterization
of fair subtyping that we introduced later in [Ciccone et al., 2022].
<Ref>, <Ref> show the type systems that have been presented in [Ciccone et al., 2022]
and in [Ciccone and Padovani, 2022], respectively.

The Agda library for (Generalized) Inference Systems in <Ref> has been presented
in [Ciccone et al., 2021] which is based on [Ciccone, 2020].
At last, the Agda formalizations of the properties of session types in <Ref>
have been presented in [Ciccone and Padovani, 2022, Ciccone and Padovani, 2021].

Not in this thesis
In [Ciccone and Padovani, 2020] we provide an Agda mechanization of a linear $\pi$-calculus
with dependent types. One of the interesting features of such formalization is that we
can inject Agda terms in the calculus by using a proper constructor
for the terms of the calculus.
Although that work covers some topics that are related to the present thesis
($\pi$-calculus, Agda mechanization, induction/coinduction), we do not give details
about it as it falls outside the core topic the thesis.
Moreover, we are working on an Agda unification library and on
co-contextual typing inference algorithms for the linear and shared $pi$-calculus
proved to be correct in the proof assistant. Such work is based on [Zalakain and Dardha, 2021].

[Key Notions]Key Notions

CHAPTER: INTRODUCTORY NOTIONS

This chapter is dedicated to the analysis of the main notions that are treated throughout the

First, we recall the usual distinction of properties of concurrent systems in
safety and liveness ones [Owicki and Lamport, 1982].
According to the class to which it belongs, a property must be defined using a different (dual) technique.
The same happens when we want to prove the correctness of such definitions.

Then, we introduce Generalized Inference Systems [Ancona et al., 2017].
Inference systems are a well established framework in the literature to define purely (co)inductive predicates
as they provide canonical techniques for proving the correctness of a definition.
In this thesis we mainly focus on their generalization with corules in order to treat those predicates
that require a mix of induction and coinduction.

After that we move to the main topics of the thesis.
We give an overview of session types by describing what such types are and what they are used for.
In a few words, they are used to model the communication in message passing systems and to statically
enforce some desired properties. They have been originally introduced by [Honda, 1993] in a binary context
and later generalized by [Honda et al., 2008] to multiparty to deal with those scenarios
in which more entities participate to the communication.
We then review some interesting desirable properties that fall in the intersection between safety and liveness ones.

The chapter is organized as follows.
In <Ref> we review the usual classification of properties into safety and liveness ones and we
show that some fall in the intersection of the two classes.
In <Ref> we introduce generalized inference systems as a reference framework that can be used to deal with
such kind of properties.
At last, in <Ref> we introduce session types in both their binary and multiparty variants.

§ SAFETY & LIVENESS

It is well known that properties can be
distinguished between safety and liveness one.

Informally, the two classes are identified by the mottos
“nothing bad ever happens” and
“something good eventually happens” [Owicki and Lamport, 1982].

For example, in a network of communicating processes, the absence of
communication errors and of deadlocks are safety properties, whereas the fact
that a protocol or a process can always successfully terminate is a liveness

Because of their different nature, characterizations and proofs of safety and
liveness properties rely on fundamentally different (dual) techniques: safety
properties are usually based on invariance (coinductive) arguments, whereas
liveness properties are usually based on well foundedness (inductive)
arguments [Alpern and Schneider, 1985, Alpern and Schneider, 1987].

The correspondence and duality between safety/coinduction and liveness/induction
is particularly apparent when properties are specified as formulas in the modal
$\mu$-calculus [Kozen, 1983, Stirling, 2001, Bradfield and Stirling, 2007], a modal
logic equipped with least and greatest fixed points: safety properties are
expressed in terms of greatest fixed points, so that the “bad things” are
ruled out along all (possibly infinite) program executions; liveness properties
are expressed in terms of least fixed points, so that the “good things” are
always within reach along all program executions. Since the $\mu$-calculus
allows least and greatest fixed points to be interleaved arbitrarily, it makes
it possible to express properties that combine safety and liveness aspects,
although the resulting formulas are sometimes difficult to understand.

In the next examples we informally state some (co)inductive properties that
we will characterize in details in <Ref> and that we will characterize in
Agda in <Ref>.

“$\x$ belongs to the possibly infinite list $\listl$”

This is an example of a liveness property. Indeed, even if the list $\listl$ is infinite,
if $\x$ belongs to $\listl$, then we need to inspect only a finite portion of
the list. Hence, induction is required.

“All the numbers in the possibly infinite list $\listl$ are positive”

This is an example of a safety property. Indeed, in order to actually state that
a list is made of only positive numbers, we have to inspect it entirely. It is
clear that coinduction is required since the list can be infinite.

“ $\x$ is the maximum element of the possibly infinite list $\listl$”

The predicate is composed by a safety and a liveness part.

* Safety: $\x$ is greater that all the elements in $\listl$

* Liveness: $\x$ belongs to $\listl$

Hence, this property requires a mix of induction and coinduction.

§ (GENERALIZED) INFERENCE SYSTEMS

A different way of specifying (and enforcing) properties is by means of
inference systems [Aczel, 1977]. Inference systems admit two natural
interpretations, an inductive and a coinductive one respectively corresponding
to the least and the greatest fixed points of their associated inference
operator. Unlike the $\mu$-calculus, however, they lack the flexibility of
mixing their different interpretations since the inference rules are interpreted
either all inductively or all coinductively. For this reason, it is generally
difficult to specify properties that combine safety and liveness aspects by
means of a single inference system.

Generalized Inference Systems ()
[Ancona et al., 2017, Dagnino, 2019] admit a wider range of interpretations,
including intermediate fixed points of the inference operator associated with
the inference system different from the least or the greatest one.  This is made
possible by the presence of corules, whose purpose is to provide an
inductive definition of a space within which a coinductive definition is used.

Although do not achieve the same flexibility of the modal $\mu$-calculus
in combining different fixed points, they allow for the specification of
properties that can be expressed as the intersection of a least and a greatest
fixed point. This feature of resonates well with one of the fundamental
results in model checking stating that every property can be decomposed into a
conjunction of a safety property and a liveness
one [Alpern and Schneider, 1985, Alpern and Schneider, 1987, Baier and Katoen, 2008].

§.§ Definitions and interpretations

We first summarize the main notions and definitions of inference systems.
Then we generalize them by introducing (meta)corules. Given an inference
system, one has to take an interpretation that identifies
the set of defined judgments.
When dealing with a generalized inference system, such interpretation is obtained
by combining both the inductive and the coinductive ones and by
taking into account corules in the proper way.

An inference system [Aczel, 1977] $\mis$ over a universe
$\universe$ of judgments is a set of rules, which are pairs
$\RulePair\prem\judg$ where $\prem\subseteq\universe$ is the set of
premises of the rule and $\judg\in\universe$ is the conclusion of
the rule. A rule without premises is called axiom. Rules are typically
presented using the syntax

\[
\Rule\prem\judg
\]

where the line separates the premises (above the line) from the
conclusion (below the line).

Since rules may be infinite, inference systems are usually described
by using meta-rules written in a meta-language.
Informally, meta-rules group rules according to their shape.

A meta-rule $\mr$  is a tuple ,,, where

* $\MCtx$ is a set called context

* $\mpr = \ple{\mj_1,\ldots,\mj_n}$ is a finite sequence of functions
of type $\MCtx\rightarrow\universe$ called (meta-)premises

* $\mj$ is a function of type $\MCtx\rightarrow\universe$ called (meta-)conclusion

* $\sd$ is a subset of $\MCtx$  called side condition

Given $\mr=\ple{\MCtx,\ple{\mj_1,\ldots,\mj_n},\mj,\sd}$,
the inference system $\Ground{\mr}$ denoted by $\mr$ is defined by:

\[\Ground{\mr}=\{\RulePair{\{\mj_1(\mc),\ldots,\mj_n(\mc)\}}{\mj(\mc)}\mid c\in\sd\}\]

An inference meta-system $\mis$ is a set of meta-rules.
The inference system $\Ground{\mis}$ is the union of $\Ground{\mr}$ for all $\mr\in\mis$.

A predicate on $\universe$ is any subset of $\universe$. An
interpretation of an inference system $\mis$ identifies a
predicate on $\universe$ whose elements are called derivable

To define the interpretation of an inference system $\mis$, consider
the inference operator associated with $\mis$, which is the function
$\InfOp\mis : \wp(\universe) \to \wp(\universe)$ such that

\[
\InfOp\mis(X)=\set{ \judg\in\universe \mid \exists\prem\subseteq X: \RulePair\prem\judg\in\mis }
\]

for every $X \subseteq \universe$.

Intuitively, $\InfOp\mis(X)$ is the set of judgments that can be
derived in one step from those in $X$ by applying a rule of $\mis$.

Note that $\InfOp\mis$ is a monotone endofunction on the complete
lattice $\wp(\universe)$, hence it has least and greatest fixed
It can also be defined for a meta-rule
$\mr$ and an inference meta-system $\mis$ as

\[
\begin{array}{cc}
\InfOp{\mr}(X) = \set{ \mj(\mc) \mid \mc\in\sd, \mj_i(\mc) \in X \text{ for all } i \in 1..n }
\InfOp{\mis}(X) = \bigcup_{\mr\in\is} \InfOp{\mr}(X)
\end{array}
\]

The inductive interpretation $\Inductive\mis$ of an
inference system $\mis$ is the least fixed point of $\InfOp\mis$
and the coinductive interpretation $\CoInductive\mis$ is
the greatest one.

From a proof theoretical point of view, $\Inductive\mis$ and $\CoInductive\mis$
are the sets of judgments derivable with well-founded and non-well-founded proof
trees, respectively.

Generalized Inference Systems enable the definition of (some)
predicates for which neither the inductive interpretation nor the
coinductive one give the expected meaning.

A generalized inference system is a pair $\Pair\mis\mcois$ where $\mis$
and $\mcois$ are inference systems (over the same $\universe$) whose elements
are called rules and corules, respectively.

The interpretation of a generalized inference system $\Pair\mis\mcois$,
denoted by $\FlexCo\mis\mcois$, is the greatest post-fixed point of
$\InfOp\mis$ that is included in $\Inductive{\mis\cup\mcois}$.

Note that meta-corules are usually represented with a thicker line.

From a proof theoretical point of view, a $\ple{\mis,\mcois}$ identifies
those judgments derivable with an arbitrary (not necessarily well-founded) proof
tree in $\mis$ and whose nodes (the judgments occurring in the proof tree) are
derivable with a well-founded proof tree in $\mis\cup\mcois$.
For more details we refer to [Dagnino, 2019].

§.§ Proving correctness - Proof principles

The advantage of using inference systems is that they provide canonical
techniques for proving the correctness of a given definition.

Consider now a specification $\Spec\subseteq\universe$, that is an
arbitrary subset of $\universe$. We can relate $\Spec$ to the interpretation of
a (generalized) inference system using one of the following proof principles.

The induction principle <cit.> allows us to
prove the soundness of an inductively defined predicate by showing that
$\Spec$ is closed with respect to $\mis$. That is, whenever the premises
of a rule of $\mis$ are all in $\Spec$, then the conclusion of the rule is also
in $\Spec$.

$\InfOp\mis(\Spec) \subseteq \Spec$
implies $\Inductive\mis \subseteq \Spec$.

The coinduction principle <cit.> allows us
to prove the completeness of a coinductively defined predicate by showing
that $\Spec$ is consistent with respect to $\mis$.  That is, every
judgment of $\Spec$ is the conclusion of a rule whose premises are also in

$\Spec \subseteq \InfOp\mis(\Spec)$ implies $\Spec \subseteq
\CoInductive\mis$.

The bounded coinduction principle [Ancona et al., 2017] allows us
to prove the completeness of a predicate defined by a generalized
inference system $\ple{\mis,\mcois}$. In this case, one needs to show not only
that $\Spec$ is consistent with respect to $\mis$, but also that $\Spec$ is
bounded by the inductive interpretation of the inference system $\mis
\cup \mcois$. Formally:

$\Spec \subseteq \Inductive{\mis\cup\mcois}$ and
$\Spec \subseteq \InfOp\mis(\Spec)$ imply

Proving the boundedness of $\Spec$ amounts to proving the completeness of
$\mis\cup\mcois$ (inductively interpreted) with respect to $\Spec$.

§.§ Examples

We now characterize the examples from <Ref>. For the sake of simplicity
we only present the definitions and we informally state where the proof principles
are used to prove the correctness (see [Ciccone, 2020] for the detailed proofs).
In <Ref> we will show Agda mechanizations of all the definitions.
In the following we write $\listin\xs{i}$ for the i-th element of list $\xs$.

Recall the inductive property from <Ref>. Consider the inference system $\is$

(, )
(,)(, )

where the axiom states that $\x$ is inside the list containing only $\x$ while the rule tells that,
if $\x$ is inside $\xs$, then it is in the same list with an additional element $\y$.
Such inference system $\is$ must be inductively interpreted. Hence, we consider only those finite
proof trees whose leaves are applications of the axiom.

Let $\Spec = \set{(\x , \xs) \mid \exists i \in \Nat. \listin\xs{i} = \x}$.
We use the induction principle to prove the soundness of the definition
($\Inductive\is \subseteq \Spec$).

Recall the coinductive property from <Ref>. Consider the inference system $\is$

> 0

where the axiom tells that the predicate trivially holds on the empty list and the rule
states that, if a list $\xs$ is made of strictly positive numbers, then the predicate holds
on such list with an additional element $\x$ provided that $\x > 0$.
Such inference system $\is$ must be coinductively interpreted. Hence, we consider either those finite
proof trees whose leaves are the axiom or the infinite ones that are obtained by applying infinitely
many times the rule. Note that is not compulsory to interpret the rule coinductively. On the other hand,
if we interpret it inductively we obtain the expected predicate if and only if the lists under analysis are

Let $\Spec = \set{\xs \mid \forall i \in \Nat. \listin\xs{i} > 0}$.
We use the coinduction principle to prove the completeness of the definition
($\Spec \subseteq \CoInductive\is$).

Recall the property from <Ref>. We first consider the following inference system $\is$

(, )
(, )(max(, ) , )

where the axiom states that $\x$ is the maximum of the list that contains only $\x$, while the rule
states that, if $\x$ is the maximum of $\xs$, then, when we add a new number $\y$ to $\xs$, the maximum
becomes the greatest between $\x$ and $\y$.
Such inference system cannot be inductively interpreted since we have to entirely inspect a possibly infinite
list. On the other hand, the coinductive interpretation does not give us the expected meaning. Indeed, for example
we can derive $\maxelem(2 , \xs)$ where $\xs = \cons{1}\xs$ and $2$ actually does not belong to $\xs$.
The infinite proof tree is obtained by applying the rule infinitely many times.

\[
\begin{prooftree}
\[
\vdots
\justifies
\maxelem(2 , \xs)
\]
\justifies
\maxelem(2 , \cons{1}{\xs})
\end{prooftree}
\]

Hence, $\is$ characterize only the safety component of $\maxelem$ which states that the maximum must be
greater than all the elements in the list.

Now we consider the following $\cois$ consisting of a single coaxiom

(, )

Such coaxiom forces the membership of the maximum into the list.
The interpretation $\FlexCo\is\cois$ characterize the expected predicate. If we manage to find a finite proof tree
in the inductive interpretation of the inference system with the additional coaxiom it means that
the maximum belongs to the list.

Let $\Spec = \set{(\x , \xs) \mid \forall i \in \Nat. \x \geq \listin\xs{i}$ and $\member(\x , \xs)}$.
We use the bounded coinduction principle to prove the completeness of the definition
($\Spec \subseteq \FlexCo\is\cois$).

As noted at the beginning of the section, all the proofs of the examples are detailed in [Ciccone, 2020].

§ SESSION TYPES

Session types have been originally introduced by [Honda, 1993].
A session type describes the communication protocol that takes place over a
channel, namely the allowed sequences of input/output actions performed by a
process on that channel. This way it is possible to statically guarantee
some desirable properties of the communication such as
protocol fidelity, communication safety
and deadlock freedom. Original session types concerned with
the communication between two entities (binary) where each
one owns an endpoint of the channel.
They have been generalized to multiparty
by [Honda et al., 2008] to model the interaction between
multiple participants.

§.§ Binary session types

§.§ Multiparty session types

§ RELATED WORK

Now we have all the ingredients for discussing about some well known properties
that can be found in the literature.
Notably, such properties have been studied both on the pure $\pi$-calculus and
on session-based calculi. We split the discussion according the property and
the scenario under analysis.

Termination of Binary Sessions.

Termination is a liveness property that can be guaranteed when finite session
types are considered [Pérez et al., 2012]. As soon as infinite
session types are considered, many session type systems weaken the guaranteed
property to deadlock freedom.
[Lindley and Morris, 2016] define a type system for a functional
language with session primitives and recursive session types that is strongly

Liveness Properties in the $\pi$-Calculus.

[Kobayashi, 2002] defines a behavioral type system that guarantees
lock freedom in the $\pi$-calculus. Lock freedom is a liveness property akin to
progress for sessions, except that it applies to any communication
channel (shared or private).
As a paradigmatic example of lock we can consider a variant of <Ref>
in which the buyer never pays the products. Thus, the carrier
is locked.

[Padovani, 2014] adapts and extends the type system of
[Kobayashi, 2002] to enforce lock freedom in the linear
$\pi$-calculus [Kobayashi et al., 1999], into which binary sessions can
be encoded [Dardha et al., 2017].
All of these works annotate types with numbers representing finite upper bounds
to the number of interactions needed to unblock a particular input/output

Deadlock Freedom.

Deadlock freedom is a safety properties according to which a communication
cannot get stuck. A paradigmatic example of deadlocked process is (we adopt binary session
type syntax)

\[
\x\iact\Tag[true].\y\oact\Tag[false]\dots \parop \y\iact\Tag[false].\x\oact\Tag[true]\dots
\]

where we have a couple of processes running in parallel.
The former is waiting for $\Tag[true]$ on $\x$ which is sent by the second
as soon as it receives $\Tag[false]$ by the former.

[Kobayashi, 2002, Padovani, 2014] guarantee deadlock freedom using the same technique for
lock freedom.
There exist a number of session based type systems inspired by linear logic
[Wadler, 2014, Caires et al., 2016, Lindley and Morris, 2016, Carbone et al., 2016, Carbone et al., 2017]
in which deadlock freedom is dealt with
by using a process composition rule that resembles the cut rule.

Liveness Properties of Multiparty Sessions.

The enforcement of liveness properties has always been a key aspect of session
type systems, although previous works have almost exclusively focused on
progress rather than on (fair) termination.

[Scalas and Yoshida, 2019] define a general framework for
ensuring safety and liveness properties of multiparty sessions. In particular,
they define a hierarchy of three liveness predicates to characterize “live”
sessions that enjoy progress. They also point out that the coarsest liveness
property in this hierarchy, which is the one more closely related to fair
termination, cannot be enforced by their type system.

The work of [van Glabbeek et al., 2021] presents a type
system for multiparty sessions that ensures progress and is not only sound but
also complete.

[Carbone et al., 2014] characterize progress in terms
of the standard notion of lock-freedom by using catalysers.

CHAPTER: FAIR TERMINATION

Among the properties mixing safety and liveness aspects in the context of session types, we decided
to develop type systems enforcing fair termination. Such property is desirable for many reasons.
Indeed, as we briefly mentioned at the beginning of the thesis, a lock free session
does not imply that other sessions are lock free as well. On the other hand, if we consider a session and
we assume that all the other ones are fairly terminating, we can conclude that the one under analysis is
fairly terminating as well.

In <Ref> we describe the property and we relate it with other properties that are
frequently studied in the literature.
In <Ref> we formally define fair termination
in its general form on reduction systems such that it
will be instantiated in the different session type based scenarios
in <Ref>.

Notably, in <Ref> we will provide a characterization of fair termination based on generalized
inference systems (<Ref>) and we will provide a mechanization of both its definition
and correctness proofs in Agda.

§ INTRODUCTION

The decomposition of a distributed program into sessions enables its
modular static analysis and the enforcement of useful properties through a type
system. Examples of such properties are communication safety (no message
of the wrong type is ever exchanged), protocol fidelity (messages are
exchanged in the order prescribed by session types) and deadlock freedom
(the program keeps running unless all sessions have terminated). These are all
instances of safety properties, implying that “nothing bad” happens. In
general, one is also interested in reasoning and possibly enforcing
liveness properties, those implying that “something good” happens
[Owicki and Lamport, 1982]. Examples of liveness properties are junk freedom
(every message is eventually received), progress (every non-terminated
participant of multiparty a session eventually performs an action) and termination
(every session eventually comes to an end).

§.§ What

Fair termination is termination under a fairness assumption. We decided to
investigate such property since current type systems cannot deal with those scenarios
in which the communication between two entities depends on the communication between
To explain why,
we show a paradigmatic scenario that we will instantiate in different ways in the next chapters.

[Buyer - Seller - Carrier]

Consider the interaction between the following three entities:

* buyer: he can tell a seller either that he adds an item to the cart or that he pays the total amount.
We assume that the messages being sent are $\tadd$ and $\tpay$, respectively

* seller: if the buyer decides to pay the amount ($\tpay$ is received) he contacts the carrier
to ship the items. The message being sent is $\tship$

* carrier: he sends the items as soon as he is contacted by the seller ($\tship$ is received)

At the moment we do not care about the technicalities on how the three actors interact.
What makes this scenario somewhat difficult to reason
about is that the progress of the carrier is not unconditional but depends
on the choices performed by the buyer: the carrier can make progress only if
the buyer eventually pays the seller.

The fairness assumption that we used can be informally stated as

If termination is always possible, then it is inevitable

Note that <Ref> admits an infinite execution in which the buyer only
adds items to the cart and never pays the amount. Such execution is unfair
according to our assumption since the buyer can always send $\tpay$ (and terminate)
but he always avoid to do so.

§.§ Why

The reader might wonder why we focus on fair termination instead of considering
some fair version of progress. There are three reasons why we think that fair
termination is overall more appropriate than just progress.

First of all, ensuring that sessions (fairly) terminate is consistent with the
usual interpretation of the word “session” as an activity that lasts for a
finite amount of time, even when the maximum duration of the activity is
not known a priori.

Second, fair termination implies progress when it is guaranteed along
with the usual safety properties of sessions. Indeed, if the session eventually
terminates, it must be the case that any non-terminated participant (think of
the carrier waiting for a "ship" message) is guaranteed to eventually make
progress, even when such progress depends on choices made by others
(like the buyer sending "pay" to the seller).

Last but not least, fair session termination enables compositional
reasoning in the presence of multiple sessions. This is not true for progress:
if an action on a session $s$ is blocked by actions on a different session $t$,
then knowing that the session $t$ enjoys progress does not necessarily guarantee
that the action on $s$ will eventually be performed (the interaction on $t$
might continue forever). On the contrary, knowing that $t$ fairly terminates
guarantees that the action on $s$ will eventually be scheduled and performed, so
that $s$ may in turn progress towards termination.

§ FAIR TERMINATION - FORMALLY

Since the notion of fair termination will apply to several different entities in this chapter
(session types, binary and multiparty sessions, processes) here we formally define it for a generic
reduction system. Later on we will show various instantiations of this

A reduction system is a pair $(\States, {\red})$ where

* $\States$ is a set of states

* ${\red} \subseteq \States \times \States$ is a reduction relation

We adopt the following notation:

we let $C$ and $D$ range over states;

we write $C \red$ if there exists $D \in \States$ such that $C \red D$; we write
$C \nred$ if not $C \red$; we write $\wred$ for the reflexive, transitive
closure of $\red$.

We say that $D$ is reachable from $C$ if $C \wred D$.

As an example, the reduction system $(\set{A,B}, \set{(A,A),(A,B)})$
models an entity that can be in two states, $A$ or $B$, and such that the entity
may perform a reduction to remain in state $A$ or a reduction to move from state
$A$ to state $B$. To formalize the evolution of an entity from a particular
state we define runs.

A run of $C$ is a (finite or infinite) sequence
$C_0C_1\dots C_i\dots$ of states such that $C_0 = C$ and
$C_i \red C_{i+1}$ for every valid $i$. A run is maximal if
either it is infinite or if its last state $C_n$ is such that
$C_n \nred$.

Hereafter we let $\run$ range over runs. Each run in the previously defined
reduction system is either of the form $A^n$ – a finite sequence of $A$ – or
of the form $A^nB$ – a finite sequence of $A$ followed by one $B$ – or
$A^\omega$ – an infinite sequence of $A$. Among these, the runs of the form
$A^nB$ and $A^\omega$ are maximal, whereas no run of the form $A^n$ is maximal.

We now use runs to define different termination properties of states:

we say that $C$ is weakly terminating if there exists a maximal run of
$C$ that is finite;

we say that $C$ is terminating if every maximal run of $C$ is finite;

we say that $C$ is diverging if every maximal run of $C$ is infinite.

Fair termination [Francez, 1986] is a termination property that only
considers a subset of all (maximal) runs of a state, those that are considered
to be “realistic” or “fair” according to some fairness assumption.

The assumption that we make in this work, and that we stated in words in
<Ref>, is formalized thus:

A run is fair if it contains finitely many weakly terminating states.
Conversely, a run is unfair if it contains infinitely many weakly
terminating states.

Continuing with the previous example, the runs of the form $A^n$ and $A^nB$ are
fair, whereas the run $A^\omega$ is unfair. In general, an unfair run is an
execution in which termination is always within reach, but is never reached.

A key requirement of any fairness assumption is that it must be possible to
extend every finite run to a maximal fair one. This property is called
feasibility [Apt et al., 1987, van Glabbeek and Höfner, 2019] or machine
closure [Lamport, 2000].

It is easy to see that our fairness assumption is feasible:

If $\run$ is a finite run, then there exists $\run'$ such that $\run\run'$ is
a maximal fair run.

Let $D$ be the last state of $\run$. We distinguish two possibilities: if $D$
is weakly terminating, then there exists a finite maximal run $D\run'$ of $D$;
if $D$ is diverging, then there exists an infinite run $D\run'$ of $D$ such
that no state in $\run'$ is weakly terminating. In both cases we conclude by
noting that $\run\run'$ is a maximal fair run.

Fair termination is finiteness of all maximal fair runs:

We say that $C$ is fairly terminating if every maximal fair run of $C$
is finite.

In the reduction system given above, $A$ is fairly terminating. Indeed, all the
maximal runs of the form $A^nB$ are finite whereas $A^\omega$, which is the only
infinite run of $A$, is unfair.

For the particular fairness assumption that we make, it is possible to provide a
sound and complete characterization of fair termination that does not mention
fair runs. This characterization will be useful to relate fair termination with
the notion of correct session (<Ref>)
and the soundness property of the type systems we are going
to introduce in <Ref>.

Let $(\States, {\red})$ be a reduction system and $C\in\States$. Then $C$ is
fairly terminating if and only if every state reachable from $C$ is weakly

$\Rightarrow$ Let $D$ be a state reachable from $C$. That is, there exists a
finite run $\run$ of $C$ ending with $D$. By <Ref> we deduce
that this run can be extended to a maximal fair one $\run\run'$. From the
hypothesis that $C$ is fairly terminating we deduce that $\run\run'$ is
finite. Hence, $D$ is weakly terminating.

$\Leftarrow$ Let $C_0C_1\dots$ be an infinite fair run of $C$.  Using the
hypothesis we deduce that each $C_i$ is weakly terminating, which is absurd.
Hence, either there are no maximal fair runs or
every maximal fair run of $C$ is finite, but the first case is not possible
by <Ref>, thus $C$ is fairly terminating.

Most fairness assumptions have the form “if something is infinitely
often possible then something happens infinitely often” and, in this
respect, our formulation of fair run (<ref>) looks slightly
unconventional. However, it is not difficult to realize that
<ref> is an instance of the notion of fair reachability of
predicates as defined by <cit.>.
According to Queille and Sifakis, a run $\run$ is fair
with respect to some predicate $\StateSet \subseteq \States$ if, whenever in
$\run$ there are infinitely many states from which a state in $\StateSet$ is
reachable, then in $\run$ there are infinitely many occurrences of states in
$\StateSet$. When we take $\StateSet$ to be $\nred$, that is the set of
terminated states that do not reduce, pretending that irreducible states
should occur infinitely often in the run is nonsensical. So, the fairness
assumption boils down to assuming that such states should not be
reachable infinitely often, which is precisely the formulation of

§ FAIR TERMINATION AND SESSION TYPES

In this section we instantiate fair termination in session type based scenarios.

First, we consider binary sessions and then we generalize to the multiparty case.
We instantiate <Ref> as well since it will be the running example
in <Ref> and <Ref>.

For what concerns the used syntaxes and labeled transition systems, we refer to <Ref>.

We say that $S$ and $T$ are compatible, notation
$S \compatible T$, if $\Sys\S\T \wred \Sys{S'}{T'}$ implies
$\Sys{S'}{T'} \wred \Sys{\End[\co\Pol]}{\End[\Pol]}$ for some $\Pol$.

We say that a session map $M$ is coherent, notation $\coherent M$, if $M \wred N$
implies $N \wlred{\In\terminated}$.

The term “coherence” is borrowed from [Carbone et al., 2016, Carbone et al., 2017],
although the property is actually stronger than the one of
[Carbone et al., 2016, Carbone et al., 2017]
as it entails fair termination of multiparty sessions
through <ref>.

In particular, if we consider the reduction system whose states are session maps
and whose reduction relation is $\lred\tau$, then $\coherent M$ implies $M$
fairly terminating. The same applies to a $\S \compatible \T$ binary session.

The properties stated in <Ref>
are stronger than fair termination. Indeed, a deadlocked session
is fairly terminating as well as it cannot reduce.
<Ref> are equivalent to a
successful form of fair termination since we ask that the
involved sessions correctly terminate.

Now we can revise <Ref> in both scenarios.

[Binary Buyer - Seller - Carrier]

Consider the types $\S_b,\S_s$ and $\T_s,\T_c$ that model
the two binary sessions connecting buyer - seller
and seller - carrier, respectively, according to

\[
\begin{array}{lcllcl}
\S_b & = & \Out\tadd.\S_b \choice \Out\tpay.\End[\Out] \qquad & \qquad \T_s & = & \Out\tship.\End[\Out] \\
\S_s & = & \In\tadd.\S_s \choice \In\tpay.\End[\In] \qquad & \qquad \T_c & = & \In\tship.\End[\In]
\end{array}
\]

We focus on the session $\Sys{\S_b}{\S_s}$. According to
<Ref>, $\S_b$ and $\S_s$ are compatible
because, no matter how many times the buyer adds an item to the cart,
he always has the possibility to $\tpay$ the amount. The infinite
run in which the buyer only adds items is unfair according to

Note that $\S_b \compatible \S_s$ implies progress
of the session $\Sys{\T_s}{\T_c}$. Indeed, the communication between
the seller and the carrier takes place after the buyer
sends $\tpay$ which is guaranteed to happen by $\S_b \compatible \S_s$.
Furthermore, although this example can be easily adapted to the multiparty case,
it shows a very simple and realistic scenario in which more sessions are
involved, no matter if they are binary or multiparty.

<Ref> clearly holds in the multiparty context as well,
now we can model the same communication protocol using a single
multiparty session.

[Multiparty Buyer - Seller - Carrier]

Consider the session types

\[
\begin{array}{l@{~}c@{~}l}
S_b & = & \seller\Out\tadd.S_b + \seller\Out\tpay.\End[\Out]\\
S_s & = & \buyer\In\tadd.S_s + \buyer\In\tpay.\carrier\Out\tship.\End[\Out]\\
S_c & = & \seller\In\tship.\End[\In]
\end{array}
\]

which describe the behavior of the three participants
in <ref>. The session map $\Map{\buyer}{S_b} \parop
\Map{\seller}{S_s} \parop  \Map{\carrier}{S_c}$ is coherent.
The explanation is just the same as the one given in <Ref>.

Notably, in the multiparty context, fair termination implies progress
of all non terminated participants (see $\carrier$ in <Ref>).

CHAPTER: FAIR SUBTYPING

The mere assumption of fairness (see <Ref>) does not
turn an ordinary session type system into one that ensures fair session
termination because the correspondence imposed by the type system between the
structure of processes and that of the protocols they implement is generally
(often necessarily) a loose one.

Indeed, processes may be “more accommodating” than the protocols they
implement by handling more messages than those mentioned in the protocols. For
example, the seller in <Ref> could handle a $\tsearch$ message in
addition to $\tadd$ and $\tpay$, even if the session type associated with $x$
does not mention $\tsearch$.

At the same time, processes may also be “less demanding” than the protocols they
implement by sending fewer messages than those allowed by the protocols. For example,
the buyer in <Ref> could always purchase an even/odd number of items,
or at least $n$ items, or no more than $n$ items, even if the session type
associated with the channel allows sending an arbitrary number of $\tadd$ messages.

These mismatches between processes and protocols are usually reconciled by a
subtyping relation for session types [Gay and Hole, 2005, Bernardi and Hennessy, 2016].
The problem is that this subtyping relation is too coarse because
it has been conceived to preserve the
safety properties of sessions but not termination, which is a
liveness property: if session types are not sufficiently precise
descriptions of the actual behavior of processes, a session that appears to be
fairly terminating at the level of types may not terminate at all at the level
of processes.

To solve this problem we adopt fair subtyping
[Padovani, 2013, Padovani, 2016, Bravetti et al., 2021], a
liveness-preserving refinement of the subtyping relation defined by
[Gay and Hole, 2005].

The chapter is organized as follows. First, in <Ref> we present the original
subtyping relation for session types [Gay and Hole, 2005].
We conclude such section showing why such relation is unfair by applying it
to a variant of <Ref> (see <Ref>).
Then, in <Ref> we introduce fair subtyping
[Padovani, 2013, Padovani, 2016, Bravetti et al., 2021] .
We show an inference system for characterizing it and we prove its correctness
with respect to a semantic definition. At last, we
show a characterization of fair subtyping by using a generalized inference
system (see <Ref>). We will refer to this definition
in <Ref>.

§ ORIGINAL SUBTYPING

.. [us-channel-in]

.. [us-channel-out]
∀i∈I: _i _i

_i.S_i [i ∈I J]_i.T_i
∀i∈I: _i _i

[i ∈I J]_i.S_i [i ∈I]_i.T_i

Rules for subtyping [Gay and Hole, 2005]

The original subtyping relation for session types has
been introduced by [Gay and Hole, 2005] and it is obtained
by coinductively interpreting the rules in <Ref>.
Notably, we only show the relation for binary session types
since in the multiparty case it is defined in the same way and it
can be obtained by simply adapting the syntax.

The inference system in <Ref> derives judgments of
the form $\S \usubt \T$ meaning that $\S$ is a subtype
of $\T$. Let us analyze the rules in details.

Rule us-end is used to relate terminated sessions.

us-channel-in and us-channel-out relate
input and output of channels, respectively. Note that they
show a different behavior. While the former is covariant
with respect to both the channel being received and the continuation,
the second one is contravariant in the exchanged channel.

Rules us-tag-in and us-tag-out relate input
and output of message tags, respectively. Similarly to the
exchange of a channel, the former is covariant while the second
contravariant in the set of messages being exchanged.

The rules are consistent with the informal example that we gave
at the beginning of <Ref> by referring to <Ref>.
Indeed, the seller in could handle a $\tsearch$ message in
addition to $\tadd$ and $\tpay$ while the buyer
could always purchase an even/odd number of items.

Consider the session types $\S_b$ and $\S_s$ from
<Ref> describing the communication protocol between
the buyer and the seller.
We can derive

\[
\begin{array}{lcl}
\S_b = \Out\tadd.\S_b \choice \Out\tpay.\End[\Out]
& \usubt &
\S_b' = \Out\tadd\Out\tadd.\S'_b \choice \Out\tpay.\End[\Out]
\\
\S_s = \In\tadd.\S_s \choice \In\tpay.\End[\In]
& \usubt &
\S_s' = \In\tadd.\S_s' \choice \In\tpay.\End[\In]
\choice \In\tsearch.\S_s'
\end{array}
\]

We can focus on the infinite derivation trees.

\[
\begin{prooftree}
\[
\[
\vdots
\justifies
\S_b \usubt \S_b'
\]
\justifies
\Out\tadd.\S_b \choice \Out\tpay.\End[\Out] \usubt
\Out\tadd.\S_b'
\using\refrule{us-tag-out}
\]
\[
\justifies
\End[\Out] \usubt \End[\Out]
\using\refrule{us-end}
\]
\justifies
\Out\tadd.\S_b \choice \Out\tpay.\End[\Out] \usubt
\Out\tadd\Out\tadd.\S'_b \choice \Out\tpay.\End[\Out]
\using\refrule{us-tag-out}
\end{prooftree}
\]

\[
\begin{prooftree}
\[
\vdots
\justifies
\S_s \usubt \S_s'
\]
\[
\justifies
\End[\In] \usubt \End[\In]
\using\refrule{us-end}
\]
\justifies
\In\tadd.\S_s \choice \In\tpay.\End[\In] \usubt
\In\tadd.\S_s' \choice \In\tpay.\End[\In]
\choice \In\tsearch.\S_s'
\using\refrule{us-tag-in}
\end{prooftree}
\]

As previously noted, the same judgments can be derived
for the multiparty session types in <Ref>.

The subtyping relation we presented induces a substitution

If $\S \usubt \T$, then a process that uses an endpoint according
to $\S$ can be safely substituted with a process that
uses the endpoint according to $\T$.

Note that we highlight the word safe as we want to
point out that the subtyping relation under analysis is
studied to preserve the safety of the communication.
We will give more details in <Ref>.

The reader might be confused by the formulation of <Ref>
as it seems to treat the substitution in the wrong direction
(left-to-right). However, it is important to think about the
subject of the principle, processes in <Ref>.
Indeed, the same principle
can be formulated in a right-to-left fashion as in [Liskov and Wing, 1994]
by taking into account the endpoints and not the processes.
The two formulations turn out to be equivalent (see [Gay, 2016] for
more details).

§.§ Unfair Subtyping

In <Ref> we pointed out the safety-preserving
property of <Ref>.
Indeed, the two substitutions proposed in <Ref>
do not break the correctness of the communication between the entities.

However, the subtyping relation introduced by [Gay and Hole, 2005]
can break the liveness of the session on which it is applied.

Consider the session types $\S_b$ and $\S_s$ from <Ref>.
The following judgment can be derived

\[
\begin{array}{lclclcl}
\S_b & = 			& \Out\tadd.\S_b \choice \Out\tpay.\End[\Out]
& \usubt & \S_b^\infty
& = 			& \Out\tadd.\S_b^\infty
\end{array}
\]

Let us look at the infinite derivation tree

\[
\begin{prooftree}
\[
\[
\vdots
\justifies
\S_b \usubt \S_b^\infty
\using\refrule{us-tag-out}
\]
\justifies
\S_b \usubt \S_b^\infty
\using\refrule{us-tag-out}
\]
\justifies
\Out\tadd.\S_b \choice \Out\tpay.\End[\Out] \usubt
\Out\tadd.\S_b^\infty
\using\refrule{us-tag-out}
\end{prooftree}
\]

As a consequence, buyer can be replaced with
buyer$_\infty$ behaving as $\S_b^\infty$
by using <Ref> (it only $\tadd$s items).
No matter how it reduces,
the buyer$_\infty$ will never $\tpay$ the amount and the
session will never terminate. Moreover, the only run of the
session is infinite and fair since it does not contain
any weakly terminating state.

This example applies to <Ref> as well.

Intuitively, the problem of the subtyping we investigated so far lies
in the contravariance of the output rule us-tag-out.
When such rule is applied, some branches are cut and it might happen
that all those branches leading to termination are removed.
This is what happens in <Ref>.
Hence, the subtyping of [Gay and Hole, 2005] must be refined
to preserve the termination property of the session.

§ FAIR SUBTYPING

Fair subtyping is a liveness-preserving variant
of the subtyping proposed by [Gay and Hole, 2005].
In this section we present such relation as a purely
coinductive predicate. However, in <Ref>
we will show an equivalent and more involved formulation
obtained by equipping the rules in <Ref> with
a corule (see <Ref>). While the generalized
inference system is intriguing since it points out the safety
and liveness aspects of the predicate, the formulation we give in
this section significantly simplifies the correctness proofs and
it will be easily integrated in the type systems in <Ref>.
Since binary sessions are the simplest multiparty ones, we refer to the binary
case when it allows to simplify the presentation of some features of the property
(examples, description of the rules) while we present all the results
in the more general multiparty one.

[n]  [fsb-end]
∀i∈I: S_i [n_i] T_i

∀i∈I: n_i ≤n

_i.S_i [n] [i∈I J]_i.T_i

S [n] T

U.S [n] U.T
∀i∈I: S_i [n_i] T_i

∀i∈I: n_i ≤n

[i∈I]_i.S_i [n] _i.T_i
∀i∈I: S_i [n_i] T_i

∃i∈I: n_i < n

[i ∈I J]_i.S_i [n] _i.T_i

Inference system for fair subtyping - Binary

[n]  [fsm-end]
∀i∈I: S_i [n_i] T_i

∀i∈I: n_i ≤n

_i.S_i [n] [i∈I J]_i.T_i
S [n] T

U.S [n] U.T
∀i∈I: S_i [n_i] T_i

∀i∈I: n_i ≤n

[i∈I]_i.S_i [n] _i.T_i
∀i∈I: S_i [n_i] T_i

∃i∈I: n_i < n

[i ∈I J]_i.S_i [n] _i.T_i

Inference system for fair subtyping - Multiparty

Fair subtyping for binary session types is defined as the
relation $\subt[n]$ coinductively defined by the inference system
in <Ref>, where $n$ ranges over natural numbers. The characterization
of fair subtyping that we consider is the relation ${\subt} \eqdef
\bigcup_{n\in\Nat} {\subt[n]}$.
Fair subtyping for multiparty session types is analogously defined
(see <Ref>).

The rules for deriving $S \subt[n] T$ are quite similar to those of the standard
subtyping relation for session types [Gay and Hole, 2005]: fsb-end states
reflexivity of subtyping on terminated session types; fsb-channel
relates higher-order session types with the same polarity and payload type;
fsb-tag-in is the usual covariant rule for the input of tags (the set
of tags in the larger session type includes those in the smaller one);
fsb-tag-out-2 is the usual contravariant rule for the output of tags
(the set of tags in the smaller session type includes those in the larger one).
Overall, these rules entail a “simulation” between the behaviors described by
$\S_b$ and $\S_b'$ whereby all inputs offered by $\S_b$ are also offered by $\S_b'$ and all
outputs performed by $\S_b'$ are also performed by $\S_b$.

The main differences between $\subt$ and the subtyping relation of [Gay and Hole, 2005]
are the presence of an invariant rule for outputs
fsb-tag-out-1 and the natural number $n$ annotating each subtyping
judgment $S \subt[n] T$. Intuitively, this number estimates how much $\S_b$ and $\S_b'$
differ in terms of performed outputs. In all rules but fsb-tag-out-2,
the annotation in the conclusion of the rule is just an upper bound of the
annotations found in the premises. In fsb-tag-out-2, where the sets of
output tags in related session types may differ, the annotation $n$ is required
to be a strict upper bound for at least one of the premises. That is,
there must be at least one premise in which the annotation strictly decreases,
while no restriction is imposed on the others. Intuitively, this ensures the
existence of a tag shared by the two related session types whose corresponding
continuations are slightly less different. So, the annotation $n$ provides an
upper bound to the number of applications of fsb-tag-out-2 along any
path (any sequence of actions) shared by $\S_b$ and $\S_b'$ that leads to
termination.  In the particular case when $n=0$, the rule fsb-tag-out-2
cannot be applied, so that $\S_b'$ may perform all the outputs also performed by

As it can be noted from fsb-channel and fsm-channel,
we require that the type of the channel being exchanged in the supertype
matches that in the subtype. We made such a decision
since we found out that allowing co/contravariance of input/output of channels
may break the liveness of the session.
We will give more details in <Ref>.

Fair subtyping allows us to reject the subtyping instance in <Ref>
that breaks the liveness of the involved session.

Consider the session types

\[
\begin{array}{rclrcl}
S_b & = & \Out\tadd.S_b + \Out\tpay.\End[\Out]
\qquad &
\S_b' & = & \Out\tadd.\Out\tadd.\S_b' + \Out\tpay.\End[\Out]
\end{array}
\]

from <Ref>
describing the buyer purchasing an arbitrary number of items
and the behavior of the buyer always purchasing an even
number of items, respectively. Consider also

\[
\S_b^\infty = \Out\tadd.\S_b^\infty
\]

from <Ref>,
which describes the behavior of a buyer attempting to $\tadd$ an
infinite number of items without ever $\tpay$ing the seller.

We have $\S_b \subt \S_b'$ and $\S_b \not\subt \S_b^\infty$. Indeed, we can derive

\[
\begin{prooftree}
\[
\[
\mathstrut\smash\vdots
\justifies
\S_b \subt[1] \S_b'
\]
\justifies
\S_b \subt[2] \Out\tadd.\S_b'
\using\refrule{fsb-tag-out-2}
\]
\[
\justifies
\End[\Out] \subt[0] \End[\Out]
\using\refrule{fsb-end}
\]
\justifies
\S_b \subt[1] \S_b'
\using\refrule{fsb-tag-out-2}
\end{prooftree}
\]

but there is no derivation for $\S_b \subt[n] \S_b^\infty$ no matter how large $n$ is

Note that there are infinitely many sequences of actions of $\S_b$ that cannot be
performed by both $\S_b'$ and $\S_b^\infty$. In particular, $\S_b'$ cannot perform any sequence
of actions consisting of an odd number of $\Tag[add]$ outputs followed by a
$\Tag[pay]$ output, whereas $\S_b^\infty$ cannot perform any sequence of $\Tag[add]$
outputs followed by a $\Tag[pay]$ output. Nonetheless, there is a path shared
by $\S_b$ and $\S_b'$ that leads into a region of $\S_b$ and $\S_b'$ in which no more
differences are detectable. The annotations in the derivation tree measures
the distance of each judgment from such region. In the case of $\S_b$ and $\S_b^\infty$,
there is no shared path that leads to a region where no differences are

Consider the session types

\[
\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}
\]

the behavior of two slot machines, an unbiased one in which the player may win
at every play and a biased one in which the player never wins. If we try to
build a derivation for $S \subt[n] T$ we obtain

\[
\begin{prooftree}
\[
\[
\mathstrut\smash\vdots
\justifies
S \subt[n-1] T
\]
\justifies
\Out\twin.S + \Out\tlose.S \subt[n] \Out\tlose.T
\using\refrule{f-tag-out-1}
\]
\[
\justifies
\End[\Out] \subt[n] \End[\Out]
\using\refrule{f-end}
\]
\justifies
S \subt[n] T
\using\refrule{f-tag-in}
\end{prooftree}
\]

which would contain an infinite branch with strictly decreasing annotations.
Therefore, we have $S \not\subt T$.

In this case there exists a shared path leading into a region of $S$ and $T$
in which no more differences are detectable between the two protocols, but
this path starts from an input. The fact that $S$ is not a fair subtype
of $T$ has a semantic justification. Think of a player that deliberately
insists on playing until it wins. This is possible when the player interacts
with the unbiased slot machine $S$ but not with the biased one $T$.

Now we can provide a semantic characterization of fair subtyping for binary and multiparty
session types as the relation preserving compliance (<Ref>) and
coherence (<Ref>) of the involved session, respectively.
Since the notion of coherence boils down to compatibility when there
are exactly two participants, we only state the property in the multiparty scenario.

We say that $\S$ is a fair subtype of $\T$, notation
$\S \ssubt \T$, if $M \parop \Map\role\S$ coherent implies
$M \parop \Map\role\T$ coherent for every $M$ and $\role$.

We conclude this section by stating and proving a fundamental property of
fair subtyping.

$\subt$ is a preorder.

While reflexivity of $\subt$ is trivial to prove (since fsm-tag-out-2 is
never necessary, it suffices to only consider judgments with a $0$ annotation),
transitivity is surprisingly complex. The challenging part of proving that from
$S \subt[m] U$ and $U \subt[n] T$ we can derive $S \subt[k] T$ is to come up
with a feasible annotation $k$. As it turns out, such $k$ depends not only on
$m$ and $n$, but also on annotations found in different regions of the
derivation trees that prove $S \subt[m] U$ and $U \subt[n] T$. In particular,
the “difference” of $S$ and $T$ is not simply the “maximum difference” or
“the sum of the differences” of $S$ and $U$ and of $U$ and $T$.

More in detail, we first show that we can always find a derivation of $S\subt[m]
U$ where the rank annotations of all judgements occurring in it are below some
$h \geq m$; then, the judgement $S\subt[k] T$ is provable for $k = m + (1+h)n$.

Let $S \subt[n]^m T$ if and only if $S \subt[n] T$ is the
conclusion of a derivation in which every rank annotation is at
most $m$. Then $S \subt[n] T$ if and only $S \subt[n]^m T$ for
some $m$.

The “if” part is obvious. Concerning the “only if” part, it
suffices to show that each judgment in the set

\[
\srel \eqdef \set{U \subt[m] V \mid U \subt[m] V \wedge \nexists
n < m: U \subt[n] V}
\]

is derivable from premises that are also in $\srel$. This is
enough to prove $S \subt[n]^m T$ from $S \subt[n] T$, because in
$\srel$ there is at most one judgment $U \subt[n] V$ for each pair
of session types $U$ and $V$ and, by regularity of $U$ and $V$,
the derivation of $U \subt[n] V$ obtained using judgments in
$\srel$ contains finitely many annotations, which must have a

Suppose $U \subt[m] V \in \srel$. Then $U \subt[m] V$ is
derivable. We reason by cases on the last rule applied to derive
this judgment.

Then $U = V = \End$ and there is nothing left to prove since
fsm-end has no premises.

Then $U = \Tags\role\In\Tag_i.U_i$ and
$V = \Tags[i\in J]\role\In\Tag_i.V_i$ and $I \subseteq J$ and
$U_i \subt[n_i] V_i$ and $n_i \leq m$ for every $i\in I$.

By definition of $\srel$ we have that, for every $i\in I$, there
exists $m_i \leq n_i$ such that $U \subt[m_i] V_i \in \srel$.

Then $U \subt[m] V$ is derivable by fsm-tag-in using
premises in $\srel$.

Analogous to the previous case.

Then $U = \Tags\role\Out\Tag_i.U_i$ and
$V = \Tags[i\in J]\role\Out\Tag_i.V_i$ and $J \subseteq I$ and
$U_i \subt[n_i] V_i$ for every $i\in J$ and $n_k < m$ for some
$k\in I$.

By definition of $\srel$ we have that, for every $i\in J$, there
exists $m_i \leq n_i$ such that $U \subt[m_i] V_i \in \srel$.

In particular, $m_k \leq n_k < m$.

Then $U \subt[m] V$ is derivable by fsm-tag-out-2 using
premises in $\srel$.

The proof that $\subt$ is reflexive is trivial, since
$S \subt[n] S$ is derivable for every $n$. Concerning
transitivity, by <ref> it suffices to show
that each judgment in the set

\[
\srel \eqdef \set{
S \subt[n_1 + (1 + m)n_2] T \mid S \subt[n_1]^m U \wedge U \subt[n_2] T
\]

is derivable using the rules in <Ref> from premises that
are also in $\srel$.

Suppose $S \subt[n] T \in \srel$. Then there exist $U$, $n_1$, $m$
and $n_2$ such that $S \subt[n_1]^m U$ and $U \subt[n_2] T$ and
$n = n_1 + (1 + m)n_2$.

We reason by cases on the last rules applied to derive
$S \subt[n_1] U$ and $U \subt[n_2] T$.

Then $S = U = T = \End$ hence $S \subt[n] T$ is derivable by fsm-end.

Then $S = \Tags\role\In\Tag_i.S_i$ and $U = \Tags[i\in J]\role\In\Tag_i.U_i$
and $T = \Tags[i\in K]\role\In\Tag_i.T_i$ and $I \subseteq J \subseteq K$ and
$S_i \subt[n_{1i}]^m U_i$ and $n_{1i} \leq n_1$ for every $i\in I$ and $U_i
\subt[n_{2i}] T_i$ and $n_{2i} \leq n_2$ for every $i\in J$.

By definition of $\srel$ we have that $S_i \subt[n_{1i} + (1 + m)n_{2i}] T_i
\in \srel$ for every $i\in I$.

Observe that $n_{1i} + (1 + m)n_{2i} \leq n_1 + (1 + m)n_2 = n$ for every
$i\in I$ hence $S \subt[n] T$ is derivable by fsm-tag-in.

Then $S = \Tags\role\Out\Tag_i.S_i$ and
$U = \Tags\role\Out\Tag_i.U_i$ and $T = \Tags\role\Out\Tag_i.T_i$
and $S_i \subt[n_{1i}]^m U_i$ and $n_{1i} \leq n_1$ and
$U_i \subt[n_{2i}] T_i$ and $n_{2i} \leq n_2$ for every $i\in I$.

By definition of $\srel$ we have that
$S_i \subt[n_{1i} + (1 + m)n_{2i}] T_i \in \srel$ for every
$i\in I$.

Observe that $n_{1i} + (1 + m)n_{2i} \leq n_1 + (1 + m)n_2 = n$
for every $i\in I$ hence $S \subt[n] T$ is derivable by

Case fsm-tag-out-1 and fsm-tag-out-2

Then $S = \Tags\role\Out\Tag_i.S_i$ and
$U = \Tags\role\Out\Tag_i.U_i$ and
$T = \Tags[i\in J]\role\Out\Tag_i.T_i$ and $J \subseteq I$ and
$S_i \subt[n_{1i}]^m U_i$ and $n_{1i} \leq n_1$ for every $i\in I$
and $U_i \subt[n_{2i}] T_i$ for every $i\in J$ and $n_{2k} < n_2$
for some $k\in J$.

By definition of $\srel$ we have that
$S_i \subt[n_{1i} + (1 + m)n_{2i}] T_i \in \srel$ for every
$i\in J$.

Observe that $n_{1k} + (1 + m)n_{2k} < n_1 + (1 + m)n_2 = n$ hence
$S \subt[n] T$ is derivable by f-tag-out-2.

Case fsm-tag-out-2 and fsm-tag-out-1

Then $S = \Tags\role\Out\Tag_i.S_i$ and
$U = \Tags[i\in J]\role\Out\Tag_i.U_i$ and
$T = \Tags[i\in J]\role\Out\Tag_i.T_i$ and $J \subseteq I$ and
$S_i \subt[n_{1i}]^m U_i$ for every $i\in J$ and $n_{1k} < n_1$
for some $k\in J$ and $U_i \subt[n_{2i}] T_i$ for every $i\in J$
and $n_{2i} \leq n_2$ for every $i\in J$.

By definition of $\srel$ we have that
$S_i \subt[n_{1i} + (1 + m)n_{2i}] T_i \in \srel$ for every
$i\in J$.

Observe that $n_{1k} + (1 + m)n_{2k} < n_1 + (1 + m)n_2 = n$ hence
$S \subt[n] T$ is derivable by fsm-tag-out-2.

Then $S = \Tags\role\Out\Tag_i.S_i$,
$U = \Tags[i\in J]\role\Out\Tag_i.U_i$ and
$T = \Tags[i\in K]\role\Out\Tag_i.T_i$ and
$K \subseteq J \subseteq I$ and $S_i \subt[n_{1i}]^m U_i$ for
every $i\in J$ and $n_{1j} < n_1$ for some $j\in J$ and
$U_i \subt[n_{2i}] T_i$ for every $i\in K$ and $n_{2k} < n_2$ for
some $k\in K$.

By definition of $\srel$ we have that
$S_i \subt[n_{1i} + (1 + m)n_{2i}] T_i \in \srel$ for every
$i\in K$.

Observe that

\[
\begin{array}{rcll}
n_{1k} + (1 + m)n_{2k} & \leq & m + (1 + m)n_{2k} & \text{since $n_{1k} \leq m$}
\\
& < & 1 + m + (1 + m)n_{2k}
\\
& = & (1 + m)(1 + n_{2k})
\\
& \leq & (1 + m)n_2 & \text{since $n_{2k} < n_2$}
\\
& < & n_1 + (1 + m)n_2 & \text{since $n_{1j} < n_1$}
\end{array}
\]

hence $S \subt[n] T$ is derivable by fsm-tag-out-2.

§.§ Correctness - Soundness

Now we prove the soundness of $\subt$ with respect
to $\ssubt$ (<Ref>). That is, we prove that $\subt$
is coherence-preserving just like $\ssubt$ is.
The proof of this result relies on a key property of $\subt$ not enjoyed by the
usual subtyping relation on session types [Gay and Hole, 2005]: when $S\subt T$ and
$M \parop \Map\rolep S$ is coherent, the session map $M \parop \Map\rolep T$ can
successfully terminate (<Ref>).
The rank annotation on subtyping judgements is used to
set up an appropriate inductive argument for proving this property.

If $S \subt T$ then $S \ssubt T$.

We start with an auxiliary result formalizing the simulation entailed by the
relation $S \subt T$.

If $S \subt T$ and $M \parop \Map\rolep{S}$ is coherent and $M \parop
\Map\rolep{T} \wred N \parop \Map\rolep{T'}$, then $M \parop \Map\rolep{S}
\wred N \parop \Map\rolep{S'}$ for some $S' \subt T'$.

We prove the result for a single reduction
$M \parop \Map\rolep{T} \lred\tau N \parop \Map\rolep{T'}$. The
general statement then follows by a straightforward induction on
the length of the reduction
$M \parop \Map\rolep{T} \wred N \parop \Map\rolep{T'}$ using the
fact that coherence is preserved by reductions.

Case $M \lred\tau N$

Then $T' = T$ and we conclude by taking $S' \eqdef S$.

Case $\Map\rolep{T} \lred\tau \Map\rolep{T''}$

$\Map\rolep{T} = \Map\rolep{\Tags\roleq\Out\Tag_i.T_i} \lred\tau
\Map\rolep{\roleq\Out{\Tag_k}.T_k} = \Map\rolep{T'}$ for
some $k\in I$.

From the hypothesis $S \subt T$ we deduce
$S = \Tags[i\in J]\roleq\Out\Tag_i.S_i$ where $I \subseteq J$ and
$S_i \subt T_i$ for every $i\in I$.

Now we have
$M \parop \Map\rolep{S} \lred\tau M \parop
\Map\rolep{\roleq\Out\Tag_k.S_k}$ and also
$\roleq\Out\Tag_k.S_k \subt T'$.

We conclude by taking $S' \eqdef \roleq\Out\Tag_k.S_k$.

Case $M \xlred{\Map\roleq{\rolep\Out\Tag}} N$ and
$\Map\rolep{T} \xlred{\Map\rolep{\roleq\In\Tag}}
\Map\rolep{T'}$

Then $T = \Tags\roleq\In\Tag_i.T_i$ and $\Tag = \Tag_k$ and
$T' = T_k$ for some $k\in I$.

From the hypothesis $S \subt T$ we deduce
$S = \Tags[i\in J]\roleq\In\Tag_i.S_i$ and $J \subseteq I$ and
$S_i \subt T_i$ for every $i\in J$.

From the hypothesis $M \parop \Map\rolep{S}$ coherent we deduce
$k\in J$ or else the participant $\rolep$ would not be able to
receive the $\Tag$ tag.

We conclude by taking $S' \eqdef S_k$.

Case $M \xlred{\Map\roleq{\rolep\In\Tag}} N$ and
$\Map\rolep{T} \xlred{\Map\rolep{\roleq\Out\Tag}}
\Map\rolep{T'}$

Then $T = \Tags\roleq\Out\Tag_i.T_i$ and $\Tag = \Tag_k$ and
$T' = T_k$ for some $k\in I$.

From the hypothesis $S \subt T$ we deduce
$S = \Tags[i\in J]\roleq\Out\Tag_i.S_i$ and $I \subseteq J$ and
$S_i \subt T_i$ for every $i\in I$.

We conclude by taking $S' \eqdef S_k$.

Case $M \xlred{\Map\roleq\rolep\Out U} N$ and
$\Map\rolep{T} \xlred{\Map\rolep\roleq\In U} \Map\rolep{T'}$

Then $T = \roleq\In U.T'$.

From the hypothesis $S \subt T$ we deduce $S = \roleq\In U.S'$
and $S' \subt T'$.

We conclude by observing that
$M \parop \Map\rolep{S} \lred\tau N \parop \Map\rolep{S'}$.

Case $M \xlred{\Map\roleq\rolep\In U} N$ and
$\Map\rolep{T} \xlred{\Map\rolep\roleq\Out U} \Map\rolep{T'}$

Then $T = \roleq\Out U.T'$.

From the hypothesis $S \subt T$ we deduce $S = \roleq\Out U.S'$
and $S' \subt T'$.

We conclude by observing that
$M \parop \Map\rolep{S} \lred\tau N \parop \Map\rolep{S'}$.

Next we show that $S \subt T$ preserves the termination of any session map that
completes $S$ into a coherent one.

If $S \subt[n] T$ and $M \parop \Map\rolep{S}$ is coherent, then $M \parop
\Map\rolep{T} \wlred{\In\terminated}$.

By induction on the lexicographically ordered tuple
$(n, |\actions|)$ where $\actions$ is any string of actions such
that $M \xwlred{\co\actions\co\Pol\terminated}$ and
$\Map\role{S} \xwlred{\actions\Pol\terminated}$.  We know that at
least one such $\actions$ least does exist from the hypothesis
$M \parop \Map\rolep{S}$ is coherent.

We now reason by cases on the shape of $\actions$.

Case $\actions = \varepsilon$

Then $S = \End$.

From the hypothesis $S \subt[n] T$ and fsm-end we deduce
$T = \End$ and we conclude
$M \parop \Map\rolep{T} \wlred{\In\terminated}$.

Case $\actions = \Map\rolep\roleq\In\Tag\actionsB$

Then $S = \Tags\roleq\In\Tag_i.S_i$ and $\Tag = \Tag_k$ for some
$k\in I$.

From the hypothesis $S \subt[n] T$ and fsm-tag-in we
deduce $T = \Tags[i\in J]\roleq\In\Tag_i.T_i$ and $I \subseteq J$
and $S_i \subt[n_i] T_i$ and $n_i \leq n$ for every $i\in I$.

We conclude using the induction hypothesis.

Case $\actions = \Map\rolep\roleq\Out\Tag\actionsB$

Then $S = \Tags\roleq\Out\Tag_i.S_i$ and $\Tag = \Tag_k$ for some
$k\in I$. We distinguish two sub-cases, according to the last rule
used in the derivation of $S \subt[n] T$.

If the last rule was fsm-tag-out-1, then
$T = \Tags[i\in I]\roleq\Out\Tag_i.T_i$ and $S_i \subt[n_i] T_i$
and $n_i \leq n$ for every $i\in I$.

In particular, $S_k \subt[n_k] T_k$ and $n_k \leq n$ and we
conclude using the induction hypothesis.

If the last rule was fsm-tag-out-2, then
$T = \Tags[i\in J]\roleq\Out\Tag_i.T_i$ with $J \subseteq I$ and
$S_i \subt[n_i] T_i$ for every $i\in J$ and $n_j < n$ for some
$j\in J$.

In particular, we have $S_j \subt[n_j] T_j$ and we conclude using
the induction hypothesis.

Consider a run
$M \parop \Map\rolep{T} \wred N \parop \Map\rolep{T'}$.

From <Ref> we deduce that there exists $S' \subt T'$
such that $M \parop \Map\rolep{S} \wred N \parop \Map\rolep{S'}$.

From the hypothesis that $M \parop \Map\rolep{S}$ is coherent we
deduce $N \parop \Map\rolep{S'}$ is also coherent.

From <Ref> we conclude
$N \parop \Map\rolep{T'} \wlred{\In\terminated}$.

§.§ Correctness - Completeness

<Ref> alone suffices to justify the adoption of $\subt$ as
fair subtyping relation, but we are interested in understanding to which extent
$\subt$ covers $\ssubt$. In this respect, it is quite easy to see that there
exist session types that are related by $\ssubt$ but not by $\subt$. For
example, consider $S = \role\Out\Tag[a].S$ and $T = \role\In\Tag[b].T$ and
observe that these two session types describe completely different protocols
(the output of infinitely many $\Tag[a]$'s in the case of $S$ and the input of
infinitely many $\Tag[b]$'s in the case of $T$). In particular, we have $S
\not\subt T$ and $T \not\subt S$ but also $S \ssubt T$ and $T \ssubt S$. That
is, $S$ and $T$ are unrelated according to $\subt$ but they are
equivalent according to $\ssubt$. This equivalence is justified by the
fact that there exists no coherent session map in which $S$ and $T$ could play
any role, because none of them can ever terminate.

This discussion hints at the possibility that, if we restrict the attention to
those session types that can terminate, which are the interesting ones as
far as this work is concerned, then we can establish a tighter correspondence
between $\subt$ and $\ssubt$. We call such session types bounded, because
they describe protocols for which termination is always within reach.

We say that a session type is bounded if all of its subtrees contain a
$\End$ leaf.

Note that a finite session type is always bounded but not every bounded
session type is finite. If we consider the reduction system in which states are
session types and we have $S \red T$ if $T$ is an immediate subtree of $S$, then
$S$ is bounded if and only if $S$ is fairly terminating.

Now, for the family of bounded session types we can prove a relative
completeness result for $\subt$ with respect to $\ssubt$.

$S$ bounded, $S \ssubt T$ imply $S \subt T$.

The proof of <Ref> is done by contradiction. We show
that, for any bounded $S$, if $S\subt T$ does not hold then we can build a
session map $M$ called discriminator such that $M\parop \Map\rolep S$ is
coherent and $M\parop \Map\rolep T$ is not, which contraddicts the hypothesis $S
\ssubt T$.

The boundedness of $S$ is necessary to make sure that it is always possible to
find a session map $N$ such that $N\parop \Map\rolep S$ is coherent.

For this proof we need some auxiliary notions and notation.

First of all, we consider unfair subtyping $\usubt$ from
<Ref> and we fix the invariance of the type of the
channel being sent by substituting rules us-channel-in
and us-channel-out with

\[
\inferrule[us-channel]{
S \usubt T
\role\Pol U.S \usubt \role\Pol U.T
\]

It is straightforward to see that ${\subt} \subseteq {\usubt}$.
Then, we introduce some convenient notation for building session maps. To do
this, we assume the existence of an arbitrary total order $<$ on the set of

Now, given a finite set of roles $\set{\role_1,\dots,\role_n}$ where $\role_1 <
\cdots < \role_n$, we write $\set{\role_1,\dots,\role_n}\Out\Tag.S$ for the
session type $\role_1\Out\Tag\cdots\role_n\Out\Tag.S$.

Given a finite family $\set{M_i}_{i\in I}$ of session maps all having the same
domain $\set\roleq \subseteq D \subseteq \RoleSet\setminus\set\rolep$, we write
$\Map\roleq{\Tags{\rolep\Pol\Tag_i.M_i}}$ for the session map $M$ having domain
$D$ and such that

\[
M(\roler) \eqdef
\begin{cases}
\Tags\rolep\Pol\Tag_i.  D\setminus\set{\roleq}\Out\Tag_i.
M_i(\roleq) & \text{if $\roler = \roleq$}
\\
\Tags\roleq\In\Tag_i.M_i(\roler) & \text{if
$\roler \neq \roleq$}
\end{cases}
\]

for every $\roler \in D$.

As suggested by the notation, this session map realizes a conversation in which
$\roleq$ first interacts with $\rolep$ by exchanging a tag $\Tag_i$ and then it
informs all the other participants about the tag that has been exchanged. This
session map has the property

\[
M \xlred{\roleq:\rolep\Pol\Tag_k}\wred M_i
\]

for every $k\in I$.

Similarly, given a session map $N$ with domain $D \supseteq\set\roleq$, we write
$\Map{\roleq}{\rolep\Pol{U}.N}$ for the session map $M$ with domain $D$ such

\[
M(\roler) \eqdef
\begin{cases}
\rolep\Pol{U}.N(\roleq) & \text{if $\roler = \roleq$}
\\
N(\roler) & \text{if $\roler \in D\setminus\set{\rolep,\roleq}$}
\end{cases}
\]

for every $\roler \in D$. Note that $M$ has the property

\[
M \xlred{\roleq:\rolep\Pol{U}} N
\]

The first key step is showing that $S \ssubt T$ implies $S \usubt T$ when $S$ is
a bounded session type. That is, unfair subtyping is a necessary
condition for fair subtyping to hold.

If $S$ is bounded and $S \ssubt T$ then $S \usubt T$.

Using the coinduction principle (<Ref>)
it suffices to show that each judgment in the set

\[
\srel \eqdef \set{ S \usubt T \mid \text{$S$ is bounded and $S \ssubt T$} }
\]

is derivable by the rules in <Ref> from premises that
satisfy the same property. Let $S \usubt T \in \srel$. Then $S$ is
bounded and $S \ssubt T$.

We reason by cases on the shape of $S$.

Case $S = \End$

Consider $M \eqdef \Map{\roleq}{\End[\co\Pol]}$ and observe that
$M \parop \Map{\rolep} S$ is coherent. Then $M \parop \Map{\rolep} T$ is
coherent as well, which implies $T = \End$.

We conclude by observing that $\End \usubt \End$ is derivable with

Case $S = \Tags\roleq\Out\Tag_i.S_i$

Let $\set{M_i}_{i\in I}$ be a family of session maps such that
$M_i \parop \Map{\rolep} S_i$ is coherent for every $i\in I$. Such
family is guaranteed to exist from the hypothesis that $S$ is

Without loss of generality we may assume that the $M_i$ all have
the same domain $D \supseteq \set\roleq$.

Let $M \eqdef \Map{\roleq}{\Tags\rolep\In\Tag_i.M_i}$ and observe that
$M \parop \Map{\rolep}{S}$ is coherent by definition of $M$.  Then
$M \parop \Map{\rolep}{T}$ is coherent as well.

We deduce that $T = \Tags[i\in J]\roleq\Out\Tag_i.T_i$ and
$J \subseteq I$ and also that $M_i \parop \Map{\rolep}{T_i}$ is coherent
for every $i\in J$. Hence $S_i \ssubt T_i$ for every $i\in J$,
namely $S_i \usubt T_i \in \srel$ for every $i\in J$ by definition
of $\srel$.

We conclude by observing that $S \usubt T$ is derivable by

Case $S = \Tags\roleq\In\Tag_i.S_i$

Let $\set{M_i}_{i\in I}$ be a family of session maps such that
$M_i \parop \Map{\rolep}{S_i}$ is coherent for every $i\in I$. Such
family is guaranteed to exist from the hypothesis that $S$ is
bounded. Without loss of generality we may assume that the $M_i$
all have the same domain $D \supseteq \set\roleq$.

Let $M \eqdef \Map{\roleq}{\Tags\rolep\Out\Tag_i.M_i}$ and observe that
$M \parop \Map{\rolep}{S}$ is coherent by definition of $M$.

We deduce that $T = \Tags[i\in J]\roleq\In\Tag_i.T_i$ and
$I \subseteq J$ and also that $M_i \parop \Map{\rolep}{T_i}$ is coherent
for every $i\in I$. Hence $S_i \ssubt T_i$ for every $i\in I$,
namely $S_i \usubt T_i \in \srel$ for every $i\in I$ by definition
of $\srel$.

We conclude by observing that $S \usubt T$ is derivable by

Case $S = \roleq\Pol{U}.S'$

Let $N$ be a session map such that $N \parop \Map{\rolep}{S'}$ is
coherent. Such $N$ is guaranteed to exist from the hypothesis that
$S$ is bounded.

Let $M \eqdef \Map{\roleq}{\rolep\co\Pol{U}.N}$ and observe that
$M \parop \Map{\rolep}{S}$ is coherent by definition of $M$.

We deduce that $T = \roleq\Pol{U}.T'$ and also that
$N \parop \Map{\rolep}{T'}$ is coherent. Hence $S' \ssubt T'$, namely
$S' \usubt T' \in \srel$ by definition of $\srel$.

We conclude by observing that $S \usubt T$ is derivable by

Next we show that every bounded session type may be part of a coherent session
map. This result is somewhat related to the notion of duality in binary
session type theories [Honda, 1993, Honda et al., 1998], showing that every
behavior can be completed by a matching – dual – one.

Let $\targets{\cdot}$ be the function that yields the set of roles occurring
in a session type, let $S$ be a bounded session type and $D$ be a non-empty
set of roles that includes $\targets{S}$ but not $\rolep$.

Let $\dualof\rolep{S}$ be the session map corecursively defined by
the following equations:

\[
\begin{array}{r@{~}c@{~}ll}
\dualof\rolep{\End[\In]} & = & \set{\Map\roleq \End[\Out]}_{\roleq\in D}
\\
\dualof\rolep{\End[\Out]} & = & \Map{\min D} \End[\In] \parop \set{\Map\roleq \End[\Out]}_{\roleq\in D \setminus \set{\min D}}
\\
\dualof\rolep{\Tags\roleq\Pol\Tag_i.S_i} & = &
\Map\roleq \Tags\rolep\co\Pol\Tag_i.\dualof\rolep{S_i}
\\
\dualof\rolep{\roleq\Pol{U}.S} & = &
\Map\roleq \rolep\co\Pol{U}.\dualof\rolep{S}
\end{array}
\]

$\dualof\rolep{S} \parop \Map\rolep S$ is coherent.

Follows from the definition of $\dualof\rolep{S}$.

Now we provide an algorithmic way of computing the “difference” between two
session types related by unfair subtyping.

Under the hypothesis $S\usubt T$, let $\rk(S,T)\in\N\union\set\infty$
be the least solution of the system of equations below:

\[
\begin{array}{@{}r@{~}c@{~}ll@{}}
\rk(\End, \End) & = & 0
\\
\rk(\Tags\role\In\Tag_i.S_i, \Tags[i\in J]\role\In\Tag_i.T_i)
& = & \max_{i\in I} \rk(S_i, T_i)
& I \subseteq J
\\
\rk(\Tags\role\Out\Tag_i.S_i, \Tags[i\in J]\role\Out\Tag_i.T_i)
& = & 1 + \min_{i\in J} \rk(S_i, T_i)
& J \subsetneq I
\\
\rk(\Tags\role\Out\Tag_i.S_i, \Tags\role\Out\Tag_i.T_i)
& = & \min\set{ \\
& & ~~ 1 + \min_{i\in I} \rk(S_i,T_i), \\
& & ~~ \max_{i\in I} \rk(S_i,T_i)}
\\
\rk(\role\Pol{U}.S', \role\Pol{U}.T') & = & \rk(S', T')
\end{array}
\]

To see that $\rk(S,T)$ is well defined, observe that the system of equations
defining $\rk(S,T)$ under the hypothesis $S \usubt T$ contains finitely many
equations, say $n$, by regularity of $S$ and $T$. The system is representable as
a monotone endofunction $F$ on the complete lattice $(\Nat\union\set\infty)^n$.
Thus, $F$ has a least solution of which $\rk(S,T)$ is a component.
We call two session types $S$ and $T$ divergent if they are related by unfair
subtyping and have infinite rank.

We write $S \diverge T$ if $S \usubt T$ and $\rk(S, T) = \infty$.

If $S \diverge T$ then the derivation of $S \usubt T$ contains at least one application of u-tag-out with $J \subsetneq I$ and one of the following holds:

* $S = \Tags \role\In\Tag_i.S_i$ and
$T = \Tags[i \in J] \role\In\Tag_i.T_i$ with $I \subseteq J$ and
$S_k \diverge T_k$ for some $k\in I$, or

* $S = \Tags \role\Out\Tag_i.S_i$ and
$T = \Tags[i\in J] \role\Out\Tag_j.T_j$ with $J \subseteq I$ and
$S_i \diverge T_i$ for every $i\in J$, or

* $S = \role\Pol{U}.S'$ and $T = \role\Pol{U}.T'$ and
$S' \diverge T'$.

If the derivation of $S \usubt T$ contained no application of
u-tag-out with $J \subsetneq I$ we would have
$\rk(S, T) = 0$. Now we reason by cases on the last rule used to
derive $S \usubt T$.

Then $S = T = \End$.  This case is impossible because
$\rk(\End, \End) = 0$ by definition.

Then $S = \Tags\role\In\Tag_i.S_i$ and
$T = \Tags[i\in J] \role\In\Tag_i.T_i$ with $I \subseteq J$ and
$S_i \usubt T_i$ for every $i\in I$ and
$\infty = \rk(S, T) = \max_{i\in I} \rk(S_i, T_i)$.

That is, $\rk(S_k,T_k) = \infty$ for some $k \in I$, hence we
conclude $S_k \diverge T_k$.

Then $S = \Tags\role\Out\Tag_i.S_i$ and
$T = \Tags[i\in J]\role\Out\Tag_i.T_i$ with $J \subseteq I$ and
$S_i \usubt T_i$ for every $i\in J$.

We distinguish two sub-cases.

If $J \subsetneq I$ then
$\infty = \rk(S, T) = 1 + \min_{i\in J} \rk(S_i, T_i)$, that is
$\rk(S_i, T_i) = \infty$ for every $i\in J$.

If $J = I$ then
$\infty = \rk(S, T) = \min\set{1 + \min_{i\in I} \rk(S_i, T_i),
\max_{i\in I} \rk(S_i, T_i)} \leq 1 + \min_{i\in I} \rk(S_i,
T_i)$ and we have $\rk(S_i, T_i) = \infty$ for every $i\in I$.

Therefore, in both cases, we conclude $S_i \diverge T_i$ for every
$i \in J$.

Then $S = \role\Pol{U}.S'$ and $T = \role\Pol{U}.T'$ and
$S' \usubt T'$ and $\infty = \rk(S, T) = \rk(S', T')$ hence we
conclude $S' \diverge T'$.

Finally, the key aspect of the proof of <Ref> is
how we build the session map $M$ such that $M \parop \Map{\rolep}{S}$
is coherent while $M \parop \Map{\rolep}{T}$ is not.

Let $\discriminator\rolep{S}{T}$ be the session map
corecursively defined by the following equations:

\[
\begin{array}{r@{~}c@{~}l}
\discriminator\rolep{
\Tags\roleq\In\Tag_i.S_i
\Tags[i\in J]\roleq\In\Tag_i.T_i
& = &
\Map\roleq \Tags[i\in I, S_i \diverge T_i]\rolep\Out\Tag_i.\discriminator\rolep{S_i}{T_i}
\\ & & \hfill \text{if $I \subseteq J$}
\\
\discriminator\rolep{
\Tags\roleq\Out\Tag_i.S_i
\Tags[i\in J]\roleq\Out\Tag_i.T_i
& = &
\Map\roleq \Tags[i\in J]\roleq\In\Tag_i.\discriminator\rolep{S_i}{T_i}
\\
& + & \Tags[i\in I\setminus J] \roleq\In\Tag_i.\dualof\rolep{S_i}
\\ & & \hfill \text{if $J \subseteq I$}
\\
\discriminator\rolep{
\roleq\Pol U.S
\roleq\Pol U.T
& = &
\Map\roleq \rolep\co\Pol U.\discriminator\rolep{S}{T}
\end{array}
\]

If $S$ is bounded and $S \diverge T$ then $S \not\ssubt T$.

From the hypothesis that
$S \diverge T$ and <Ref> we deduce that the
derivation of $S \usubt T$ contains at least one application of
us-tag-out with $J \subsetneq I$.

Consider $\discriminator\rolep{S}{T}$ from <Ref>.
Note that $\discriminator\rolep{S}{T}$ always sends a subset of
the labels accepted by $S$, it is willing to receive any label
sent by $S$, and it can always terminate successfully when
interacting with $S$. Note also that it terminates successfully
only after receiving a label from $S$ that $T$ cannot sent.

Therefore, we have
$\discriminator\rolep{S}{T} \parop \Map\rolep{S}$ coherent and
$\discriminator\rolep{S}{T} \parop \Map\rolep{T}$ incoherent,
which proves $S \not\ssubt T$.

Let $S \foosubt T$ if $S \usubt T$ and $\rk(U, T) < \infty$ for
every judgment $U \usubt V$ in the derivation of $S \usubt T$.

From <Ref> we have that
$S \ssubt T$ implies $S \foosubt T$. Indeed, if there is a
judgment $U \usubt V$ in the derivation of $S \usubt T$ such that
$\rk(U,V) = \infty$, then it is possible to build a session $M$
such that $M \parop \Map\role{S}$ is coherent and
$M \parop \Map\role{T}$ is not by induction on the minimum depth
of the judgment $U \usubt V$ in the derivation using the
hypothesis that $S$ is bounded and <Ref>.

Now, using the principle of coinduction, it suffices to show that
each judgment in the set

\[
\srel \eqdef \set{ S\subt[\rk(S,T)] T \mid S \foosubt T}
\]

is derivable using one of the rules in <Ref> whose
premises all belong to $\srel$.

§.§ Generalized Inference System

The purely coinductive characterization of fair subtyping
presented in <Ref> has been first used in [Ciccone et al., 2022].
Previous works
[Padovani, 2013, Padovani, 2016, Ciccone and Padovani, 2021, Ciccone and Padovani, 2022]
relied on a different characterization based on a generalized
inference system (see <Ref>) that consists of the same rules
of the original subtyping relation (<Ref>) equipped with
a corule. The generalized inference system for binary session types
is presented in <Ref>. Note the invariance in the type
of the channel being exchanged according to <Ref>.
In addition to $\subt$, we write $\isubt$ for the
relation defined by the inductive interpretation of the same inference
system and $\csubt$ for the relation defined by the coinductive
interpretation of the inference system in <ref>
excluding the corule fs-converge. We introduce the
notions of paths and residual of a session type.

∀i∈I: _i _i

_i.S_i [i ∈I J]_i.T_i

∀i∈I: _i _i

[i ∈I J]_i.S_i [i ∈I]_i.T_i

∃, :
S() T()

S T

Generalized inference system for fair subtyping

We say that $\actions$ is a path of $S$ if $S \wlred\actions$. We write
$\paths\S$ for the (prefix-closed) set of paths of $S$, that is $\paths\S
\eqdef \set{\actions \mid S \wlred\actions }$.

The residual of a session type $S$ with respect to a path $\actions \in
\paths\S$, denoted by $S(\actions)$, is the unique session type $T$ such that
$S \wlred\actions T$.

The subtle difference between fair and unfair subtyping is due to the corule
fs-converge. Since this corule is somewhat obscure,
we explain it gradually starting with the following observations:

* Recall from <Ref> that $S \subt T$ implies $S \csubt T$ and $S
\isubt T$. Hence, $\subt$ is a refinement of $\csubt$ such that, for each pair
of related session types $S$ and $T$, there exists a finite-depth
derivation tree for the judgment $S \subt T$ using the rules and possibly the
corule fs-converge.

* When $S \csubt T$ holds, it is not possible to establish a general
correlation between $\paths\S$ and $\paths\T$. Indeed, us-tag-in
entails that some paths of $T$ may not be present in $S$ and
us-tag-out entails that some paths of $S$ may not be present in $T$.

* The judgment $S \subt T$ is trivially derivable using fs-converge
if the path inclusion relation $\paths\S \subseteq \paths\T$ holds. Since
us-tag-out is the only rule that allows $T$ to have fewer paths
than $S$, we deduce that fs-converge limits (but does not always
forbid) applications of us-tag-out.

* In general fs-converge requires that, whenever a path $\actions$
of $S$ is no longer present in $T$, it must be possible to find a prefix
$\actionsB$ of $\actions$ and an output $\Out\Tag$ shared by both $S$ and $T$
such that $S(\actionsB\Out\Tag)$ and $T(\actionsB\Out\Tag)$ are one step closer to
the region of $S$ and $T$ where path inclusion holds.

The reason why path inclusion plays such an important role in the definition of
fair subtyping is that a process using a channel of type $T$ keeps using it
according to $T$ even if it is replaced by another channel of type $S \subt T$,
without even realizing that the replacement has taken place. After all, this is
what the “safe substitution principle” (<Ref>) is based on.
As a consequence, none of
the paths in $S$ that have disappeared in $T$ will be offered to the process at
the other end of the session. If there are “too few” paths in $T$ compared
to $S$, then the replacement might compromise the termination of the process at
the other end of the session, should it crucially rely on those paths to
When $S \subt T$ (and therefore $S \isubt T$) holds, the corule
fs-converge makes sure that the process using the channel of type $S$
that it has type $T$ is always at finite distance from the region where
path inclusion between (some subtrees of) $S$ and (the corresponding subtrees
of) $T$ holds. Moreover, this region is always reachable by means of
output actions (those $\Out\l$ mentioned in fs-converge) which
are performed actively by the process using the channel. In other words, the process
using such channel is always able, in a finite amount of time and relying on choices and
actions it can perform autonomously, to steer the interaction towards a region
of the protocol where path inclusion holds, hence where a common path to session
termination is guaranteed to exist.

To conclude, the generalized inference system in <Ref>
has the advantage of highlighting the liveness-preserving
feature of fair subtyping by using fs-converge. However,
the purely coinductive characterization that we gave in <Ref>
allowed us to to provide a direct proof of <Ref>.
Indeed, in previous works
[Padovani, 2013, Padovani, 2016, Ciccone and Padovani, 2021, Ciccone and Padovani, 2022],
transitivity has been established indirectly by relating the
generalized inference system of
fair subtyping with its semantic definition (<Ref>).

In <Ref> we will characterize properties of session types
mixing safety and liveness aspects. Starting from the definitions
of the safety (coinductive) parts, we will show how to use corules
to obtain the desired predicates. Hence, for what concerns
fair subtyping, we will refer to <Ref> to provide
a sound and complete Agda mechanization of such predicate (see <Ref>).

[Enforcing Fair Termination]Enforcing
Fair Termination

CHAPTER: FAIR TERMINATION OF BINARY SESSIONS

In this chapter we present the first type system for enforcing fair
termination of binary sessions. Although in <Ref> we will
present the same approach applied to multiparty ones, hence to a more general context,
the binary case succeeds in highlighting the main requirements, properties and
challenges of such a type system.

For this reason, in this chapter we focus on paradigmatic examples in order
to guide the reader across the main developed features.

In <Ref> we will show some more involved scenarios.

It is worth noting that the proof technique that we adopt to prove the soundness
of the type system is shared by both the binary and the multiparty case. However,
the two proofs differ in some technicalities (deadlock freedom).

The type system that we present in this chapter is a refined version of the one
used by [Ciccone and Padovani, 2022]. Indeed, [Ciccone and Padovani, 2022] rely on
the characterization of fair subtyping presented in <Ref>.
For the sake of uniformity with respect to [Ciccone et al., 2022] on which
<Ref> will be based on,
we refer to the purely coinductive characterization presented in <Ref>.

The chapter is organized as follows.
In <Ref> we present the syntax and the semantics of the
session based calculus on which we apply static analysis.
<Ref> shows the type system for such calculus and introduce
some additional properties that are required to enforce fair termination.
Finally, in <Ref> we detail the soundness proof the type system.

Concerning a comparison of the type system we show in this chapter with respect
to existing works, we delay the discussion to <Ref>.

§ CALCULUS

In this section we introduce the calculus for binary sessions.
We recall some basic notions.
We use an infinite set of channel names ranged over by $x$, $y$, $z$,
a set of message tags ranged over by $\Tag$, and a set of process names ranged over by
$A$, $B$, $C$.

We write $\seqof x$ for a possibly empty sequences of
channels, extending this notation to other entities and
we use $\Pol$ to range over the elements of the set $\set{\iact,\oact}$ of
polarities to distinguish input actions ($\iact$) from output actions

§.§ Syntax of Processes

§.§ Operational Semantics

§ TYPE SYSTEM

In this section we present the type system for binary sessions that we introduced in <Ref>.

Before looking at the typing rules we motivate, through a series of examples, the key properties enforced by the type system that,
taken together, guarantee fair termination. There are two families of problems that can compromise fair termination.

First of all, the process (or part thereof) may be unable to reduce further but is not $\Done$.
In our model, this can happen for many reasons, for example: a process attempts at sending a
tag on a session that the receiver is not willing to accept; a process attempts at sending a
termination signal when the receiver expects a channel; the processes at the two ends of the same
session are both waiting for a message from that session. These are all examples of safety violations,
which are prevented by any ordinary session type system.

In <Ref> we focus instead on liveness violations. Roughly
speaking, liveness is violated when a process (or part thereof) engages an
infinite computation that cannot possibly terminate.

§.§ Boundedness Properties

§.§ Typing Rules

§.§ Examples

§.§ On Higher-Order Session Types

§ PROOFS

In this section we detail the proof of <Ref>.
The most intriguing aspect in such proof is that a
closed, well-typed process admits a reduction sequence to $\Done$.

The proof technique is related to the method of helpful directions [Francez, 1986]:
we define a well-founded measure for (well-typed) processes and we prove
that this measure decreases strictly as the result of “helpful” reductions.
In our case, the measure of a (well-typed) process $P$ is a lexicographically
ordered pair $(m, n)$ of natural numbers such that $m$ is an upper bound to the
number of sessions that $P$ may need to create and of weights of casts that $P$ may need to
perform in the future in order to terminate, whereas $n$ is the
cumulative efforts to terminate the sessions that $P$ has created in the past and that
are not terminated yet.
We account for this effort by measuring the shortest reduction that terminates a
compatible session (<Ref>).
Notably, a session terminates by rb-close; a cast is
performed when it is absorbed by the corresponding restriction, namely by

We first show two standard results, that is, typing is preserved by structural
precongruence and reduction.
Then, we formally introduce the measure and we characterize some normal forms that we
need in order to achieve the proof that such measure reduces by following the right

§.§ Subject Reduction

§.§ Measure

§.§ Normal Forms

§.§ Soundness

CHAPTER: FAIR TERMINATION OF MULTIPARTY SESSIONS

In this chapter we generalize the type system in <Ref> to multiparty session types.
In particular, we provide a type system for enforcing (successful) fair termination
of multiparty sessions. In this case we refer to the notion of coherence (<Ref>).
Again, we embed fair subtyping as the coherence-preserving relation.
Notably, the boundedness properties mentioned in <Ref> are still required.
For the sake of simplicity we do not analyze them step by step as the motivating examples can be
straightforwardly adapted. Instead, we directly show how to enforce them.

The need of the type system that we present in this chapter comes from the fact the there
exist multiparty sessions that cannot be decomposed in binary ones.
Consider the following local types

\[
\begin{array}{lcl}
\S_{\rolep} & : & \roleq\Out\set{\Tag[a].\roler\Out\Tag[c].\End[\Out],\, \Tag[b].\End[\Out]}
\\
\S_{\roleq} & : & \rolep\In\set{\Tag[a].\roler\Out\Tag[ok].\End[\Out],\, \Tag[b].\roler\Out\Tag[no].\End[\Out]}
\\
\S_{\roler} & : & \roleq\In\set{\Tag[ok].\rolep\In\Tag[c].\End[\In],\, \Tag[no].\End[\In]}
\end{array}
\]

This example is paradigmatic because of the dependencies in the communications.
Indeed, $\roler$ receives $\Tag[c]$ from $\role$ only if $\roleq$ receives $\Tag[a]$ from $\role$.
Furthermore, the class of multiparty sessions that can be decomposed into linear
ones consists of those sessions whose local types can be projected to all the participants
appearing in them.
(the projections exist).
This is not true for the example above because the projections of $\S_{\role}$ on $\roler$ and
of $\S_{\roler}$ on $\role$ are not defined as is such types the communication with $\roler$ and $\role$
does not take place in all the branches.

The chapter is organized as follows.
In <Ref> we present the syntax and the semantics of the calculus based on multiparty sessions.
<Ref> shows the typing rules for such calculus. Differently from <Ref>, we focus
on some involved examples of processes instead of analyzing additional required properties (see <Ref>).
Then, in <Ref> we detail the soundness proof of the type system.
At last, in <Ref> we compare the present type system, and consequently
the one in <Ref>, to existing works.

§ CALCULUS

In this section we define the calculus for multiparty sessions on which we apply
our static analysis technique. The calculus is an extension of the one presented
by [Ciccone and Padovani, 2022] to multiparty sessions in the
style of [Scalas and Yoshida, 2019] and that has been presented in [Ciccone et al., 2022].

We recall some basic notions.
We use an infinite set of variables ranged over by $x$, $y$, $z$, an
infinite set of session names ranged over by $s$ and $t$, a set of
roles ranged over by $\rolep$, $\roleq$, $\roler$, a set of message
tags ranged over by $\Tag$, and a set of process names ranged over by
$A$, $B$, $C$. As in the binary case, the different terminology for labels
is needed to avoid confusion with the labels in <Ref>.

We use roles to distinguish the participants of a session. In particular, an
endpoint $\ep\sn\role$ consists of a session name $\sn$ and a role
$\role$ and is used by the participant with role $\role$ to interact with the
other participants of the session $s$.

We use $u$ and $v$ to range over channels, which are either variables or
session endpoints.

We write $\seqof x$ and $\seqof u$ to denote possibly empty sequences of
variables and channels, extending this notation to other entities.

We use $\Pol$ to range over the elements of the set $\set{\iact,\oact}$ of
polarities, distinguishing input actions ($\iact$) from output actions

§.§ Syntax of Processes

§.§ Operational Semantics

§.§ Examples

§ TYPE SYSTEM

In this section we describe the type system for the calculus of multiparty
sessions of <Ref>.

The typing judgments have the form $\wtp[n]\Ctx{P}$, meaning that the process
$P$ is well typed in the typing context $\Ctx$ and has rank $n$. As usual, the
typing context is a map associating channels with session types (<Ref>) and is
meant to contain an association for each name in $\fn{P}$. We write $u_1 : S_1,
\dots, u_n : S_n$ for the map with domain $\set{u_1,\dots,u_n}$ that associates
$u_i$ with $S_i$. Occasionally we write $\seqof{u : S}$ for the same context,
when the number and the specific associations are unimportant. We also assume
that endpoints occurring in a typing context have different session names. That
is, $\ep{s}\rolep, \ep{s}\roleq \in \dom\Ctx$ implies $\rolep = \roleq$.

This constraint makes sure that each well-typed process plays exactly one role
in each of the sessions in which it participates. It is also a common assumption
made in all multiparty session calculi.

We use $\Ctx$ and $\CtxD$ to range over typing contexts, we write $\EmptyCtx$
for the empty context and $\Ctx,\CtxD$ for the union of $\Ctx$ and $\CtxD$ when
they have disjoint domains and disjoint sets of session names.

The rank $n$ in a typing judgment estimates the number of sessions that
$P$ has to create and the number of casts that $P$ has to perform in order to
terminate. The fact that the rank is finite suggests that so is the effort
required by $P$ to terminate.

§.§ Typing Rules

§.§ Examples

§ CORRECTNESS

In this section we discuss the proof of <Ref>.
The proof technique follows that of <Ref>.
Such proof is essentially composed of a standard subject
reduction result showing that typing is preserved by reductions and a proof that
every well-typed process other than $\pdone$ may always reduce in such a way
that a suitably defined well-founded measure strictly decreases. The
measure is a lexicographically ordered pair of natural numbers with the
following meaning: the first component measures the number of sessions that must
be created and the total weight of casts that must be performed in order for the
process to terminate (this information is essentially the rank we associate with
typing judgments); the second component measures the overall effort required to
terminate every session that has already been created (these sessions are
identified by the fact that their restriction occurs unguarded in the process).
We account for this effort by measuring the shortest reduction that terminates a
coherent session map (<Ref>). The reason why we need two
quantities in the measure is that in general every application of fair subtyping
may increase the length of the shortest reduction that terminates a
coherent session map. So, when casts are performed the second component of the
measure may increase, but the first component reduces.

As a final remark, it should be noted that the overall measure associated with a
well-typed process may also increase, for example if new sessions are
created (<Ref>). However, one particular reduction that decreases the
measure is always guaranteed to exist.

For the sake of clarity, in the following we often write $M \ft$ instead of $\coherent M$.

§.§ Subject Reduction

§.§ Measure

§.§ Normal Forms

§.§ Soundness

§ RELATED WORK

We conclude the chapter by relating the type systems in
<Ref> to others that can be found
in the literature. In particular, we mainly recall
the references we pointed out in <Ref>.

Termination of Binary Sessions.

[Lindley and Morris, 2016] define a type system for a functional
language with session primitives and recursive session types that is strongly
normalizing. That is, a well-typed program along with all the sessions it
creates is guaranteed to terminate. This strong result is due to the fact that
the type language is equipped with least and greatest fixed point operators that
are required to match each other by duality.

Notably, strong normalization is stronger than fair termination.
As an example, <Ref> are fairly terminating but not
strongly terminating as the buyer can add arbitrarily many, possibly infinitely
many, items to the cart.

Liveness Properties in the $\pi$-Calculus.

[Kobayashi, 2002, Padovani, 2014] define a behavioral type system that guarantees
lock freedom in the $\pi$-calculus. .

These works annotate types with numbers representing finite upper bounds
to the number of interactions needed to unblock a particular input/output
action. For this reason, none of our key examples (<Ref>)
is in the scope of these analysis techniques.

[Kobayashi and Sangiorgi, 2010] show how to enforce lock
freedom by combining deadlock freedom and termination. Our work can be seen as a
generalization of this approach whereby we enforce lock freedom by combining
deadlock freedom (through a mostly conventional session type system) and
fair termination. Since fair termination is coarser than termination, the
family of programs for which lock freedom can be proved is larger as well.

Deadlock Freedom.

Our type system enforces deadlock freedom essentially thanks to the shape of the
rule tm-par (tb-par in <Ref>) which is inspired
to the cut rule of linear logic. This
rule has been applied to session type systems for binary
sessions [Wadler, 2014, Caires et al., 2016, Lindley and Morris, 2016] and
subsequently extended to multiparty
sessions [Carbone et al., 2016, Carbone et al., 2017]. In the latter
case, the rule – dubbed multiparty cut – requires a coherence condition
among cut types establishing that the session types followed by the single
participants adhere to a so-called global type describing the multiparty session
as a whole. The rule tm-par adopts the same schema, except that the
coherence condition is stronger to entail fair session termination.

The key principle of these formulations of the cut rule as a typing rule for
parallel processes is to impose a tree-like network topology, whereby two
parallel processes can share at most one channel. In the multiparty case, cyclic
network topologies can be modeled within each session (<Ref>) since
coherence implies deadlock freedom.

Having a single construct that merges session restriction and parallel
composition allows for a simple formulation of the typing rules so that dealock
freedom is easily guaranteed. However, many session calculi separate these two
forms in line with the original presentation of the $\pi$-calculus. We think
that our type system can be easily reformulated to support distinct session
restriction and parallel composition by means of
hypersequents [Kokke et al., 2018, Kokke et al., 2019].

A more liberal version of the cut rule, named multi-cut and inspired to
Gentzen's “mix” rule, is considered by [Abramsky et al., 1996]
enabling processes to share more than one channel. In this setting,
deadlock freedom is lost but can be recovered by means of a richer type structure
that keeps track of the dependencies between different channels. This approach
has been pioneered by [Kobayashi, 2002, Kobayashi, 2006] for the
$\pi$-calculus and later on refined by [Padovani, 2014].

Other approaches to ensure deadlock freedom based on
dependency/connectivity graphs that capture the network topology
implemented by processes have been studied by
[Carbone and Debois, 2010, Kobayashi and Laneve, 2017, de'Liguoro and Padovani, 2018, Jacobs et al., 2022].

Liveness Properties of Multiparty Sessions.

In [Scalas and Yoshida, 2019] the authors point out that the coarsest liveness
property in the hierarchy of liveness properties that they take into account, which is the one more closely related to fair
termination, cannot be enforced by their type system. In part, this is due to
the fact that their type system relies on a standard subtyping relation for
session types [Gay and Hole, 2005] instead of fair subtyping
[Padovani, 2013, Padovani, 2016]. As we have seen in <Ref>, even for
single-session programs the mere adoption of fair subtyping is not enough and it
is necessary to meet additional requirements.

[van Glabbeek et al., 2021] propose a type
system for multiparty sessions that ensures progress and is not only sound but
also complete. The fairness assumption they make – called justness – is
substantially weaker than our own (<Ref>) and such that the unfair
runs are those in which some interactions between participants are
systematically discriminated in favor of other interactions involving a disjoint
set of independent participants. For this reason, their progress property is in
between the two more restrictive liveness predicates of [Scalas and Yoshida, 2019]
and can only be guaranteed when it is independent
of the behavior of the other participants of the same session.

CHAPTER: LINEAR LOGIC BASED APPROACH

In this chapter we propose a type system for , a linear $\pi$-calculus with
(co)recursive types, such that well-typed processes are fairly
Our type system is a conservative extension of
[Baelde et al., 2016, Doumane, 2017, Baelde et al., 2022], the infinitary
proof system for the multiplicative additive fragment of linear logic with least
and greatest fixed points. In fact, the modifications we make to are
remarkably small: we add one (standard) rule to deal with
non-deterministic choices, those performed autonomously by a process, and
we relax the validity condition on proofs so that it only considers the
“fair behaviors” of the program it represents.

The fact that there is such a close correspondence between the typing rules of
and the inference rules of is not entirely surprising. After all,
there have been plenty of works investigating the relationship between
$\pi$-calculus terms and linear logic proofs, from those of [Abramsky, 1994],
[Bellin and Scott, 1994] to those on
the interpretation of linear logic formulas as session
types [DeYoung et al., 2012, Wadler, 2014, Caires et al., 2016, Lindley and Morris, 2016, Rocha and Caires, 2021, Qian et al., 2021].

Nonetheless, we think that the connection between and stands out
for two reasons.

First, is conceptually simpler and more general than the session-based
calculi that can be encoded in it. In particular, all the session calculi based
on linear logic rely on an asymmetric interpretation of the multiplicative
connectives $\tfork$ and $\tjoin$ so that $\FormulaF \tfork \FormulaG$
(respectively, $\FormulaF \tjoin \FormulaG$) is the type of a session endpoint
used for sending (respectively, receiving) a message of type $\FormulaF$ and
then used according to $\FormulaG$. In our setting, the connectives $\tfork$ and
$\tjoin$ retain their symmetry since we interpret $\FormulaF \tfork \FormulaG$
and $\FormulaF \tjoin \FormulaG$ formulas as the output/input of pairs, in the
same spirit of the original encoding of linear logic proofs proposed by
[Bellin and Scott, 1994]. This interpretation gives the ability of
modeling bifurcating protocols of which binary sessions are just a
special case.

The second reason why and get along has to do with the cut
elimination result for . In finitary proof systems for linear logic, cut