Ornela Dardha

Luca Padovani

Ilaria Castellani

Davide Sangiorgi

EXPRESSing Session Types

To celebrate the 30th edition of EXPRESS and the 20th edition of SOS we overview how session types can be expressed in a type theory for the standard π-calculus by means of a suitable encoding. The encoding allows one to reuse results about the π-calculus in the context of session-based communications, thus deepening the understanding of sessions and reducing redundancies in their theoretical foundations. Perhaps surprisingly, the encoding has practical implications as well, by enabling refined forms of deadlock analysis as well as allowing session type inference by means of a conventional type inference algorithm.

1 Origins of EXPRESS: some personal memories This year marks an important milestone in the history of the EXPRESS/SOS workshop series. Before joining their destinies in 2012, the two workshops EXPRESS and SOS had been running on their own since 1994 and 2004, respectively. Hence, the EXPRESS/SOS'23 workshop in Antwerp will constitute the 30th edition of EXPRESS and the 20th edition of SOS.

), Tarquinia (1995), and Dagstuhl (1996). The fourth and final workshop was held in Santa Margherita Ligure (1997). It was co-chaired by Catuscia Palamidessi and Joachim Parrow, and stood out as a distinctive event, open to external participants and organised as a conference with a call for papers. A few months after this workshop, in the first half of 1998, the co-chairs of the forthcoming CONCUR'98 conference in Nice, Robert de Simone and Davide Sangiorgi, were wondering about endowing CONCUR with a satellite event (such events were still unusual at the time) in order to enhance its attractiveness. Moreover, Davide was sharing offices with Ilaria, who had been the NoE responsible for the site of Sophia Antipolis and was also part of the organising committee of CONCUR'98. It was so, during informal discussions, that the idea of launching EXPRESS as a stand-alone event affiliated with CONCUR was conceived, in order to preserve the heritage of the NoE and give it a continuation. Thus the first edition of EXPRESS, jointly chaired by Catuscia and Ilaria, took place in Nice in 1998, as the first and unique satellite event of CONCUR. However, EXPRESS did not remain a lonely satellite for too long, as other workshops were to join the orbit of CONCUR in the following years (INFINITY, YR-CONCUR, SecCo, TRENDS, . . . ), including SOS in 2004. The workshop EXPRESS'98 turned out

to be successful and very well attended. Since then, EXPRESS has been treading its path as a regular satellite workshop of CONCUR, with a new pair of co-chairs every year, each co-chair serving two editions in a row. The workshop, which is traditionally held on the Monday preceding CONCUR, has always attracted good quality submissions and has maintained a faithful audience over the years.

Coincidentally, this double anniversary of EXPRESS/SOS falls in the 30th anniversary of Kohei Honda's first paper on session types [START_REF] Honda | Types for Dyadic Interaction[END_REF]. For this reason, we propose an overview of a particular expressiveness issue, namely the addition of session types to process calculi for mobility such as the π-calculus.

Session types and their expressiveness: introduction

Expressiveness is a key topic in the design and implementation of programming languages and models. The issue is particularly relevant in the case of formalisms for parallel and distributed systems, due to the breadth and variety of constructs that have been proposed.

Most importantly, the study of expressiveness has practical applications. If the behaviours that can be programmed by means of a certain formalism L 1 can also be programmed using another formalism L 2 , then methods and concepts developed for the latter language (e.g., reasoning and implementation techniques) may be transferred onto the former one that, in turn, may be more convenient to use from a programming viewpoint. An important instance is the case when L 2 is, syntactically, a subset of L 1 . Indeed the quest for a "minimal" formalism is central in the work on expressiveness.

This paper is an overview of a particular expressiveness issue, namely the addition of session types onto calculi for mobility such as the π-calculus. We will review the encoding of binary session types onto the standard π-calculus [START_REF] Dardha | Session types revisited[END_REF][START_REF] Dardha | Session types revisited[END_REF], based on an observation of Kobayashi [33]. The key idea of the encoding is to represent a sequence of communications within a session as a chain of communications on linear channels (channels that are meant to be used exactly once) through the use of explicit continuations, a technique that resembles the modelling of communication patterns in the actor model [START_REF] Hewitt | Viewing Control Structures as Patterns of Passing Messages[END_REF]. We discuss extensions of the encoding to subtyping, polymorphism and higher-order communication as well as multiparty session types. Finally, we review two applications of the encoding to the problems of deadlock analysis and of session type inference.

Session types, initially proposed in [START_REF] Honda | Types for Dyadic Interaction[END_REF][START_REF] Takeuchi | An Interaction-based Language and its Typing System[END_REF][START_REF] Honda | Language primitives and type disciplines for structured communication-based programming[END_REF], describe sessions, i.e., interaction protocols in distributed systems. While originally designed for process calculi, they have later been integrated also in other paradigms, including (multi-threaded) functional programming [START_REF] Vasco | Type checking a multithreaded functional language with session types[END_REF][START_REF] Pucella | Haskell session types with (almost) no class[END_REF][START_REF] Lindley | Embedding session types in Haskell[END_REF][START_REF] Orchard | Session Types with Linearity in Haskell[END_REF][START_REF] Fowler | Separating Sessions Smoothly[END_REF][START_REF] Kokke | Deadlock-free session types in linear Haskell[END_REF], component-based systems [START_REF] Vallecillo | Typing the Behavior of Software Components using Session Types[END_REF], object-oriented languages [START_REF] Dezani-Ciancaglini | Bounded Session Types for Object Oriented Languages[END_REF][START_REF] Dezani-Ciancaglini | Session Types for Object-Oriented Languages[END_REF][START_REF] Capecchi | Amalgamating sessions and methods in object-oriented languages with generics[END_REF], languages for Web Services and Contracts [START_REF] Carbone | Structured Communication-Centred Programming for Web Services[END_REF][START_REF] Montesi | Compositional Choreographies[END_REF]. They have also been studied in logical-based type systems [START_REF] Caires | Session Types as Intuitionistic Linear Propositions[END_REF][START_REF] Wadler | Propositions as sessions[END_REF][START_REF] Caires | Linear Logic Propositions as Session Types[END_REF][START_REF] Dardha | A New Linear Logic for Deadlock-Free Session-Typed Processes[END_REF][START_REF] Kokke | Prioritise the Best Variation[END_REF].

Session types allow one to describe the sequences of input and output operations that the participants of a session are supposed to follow, explicitly indicating the types of messages being transmitted. This structured sequentiality of operations makes session types suitable to model protocols. Central (type and term) constructs in session types are also branch and select, the former being the offering of a set of alternatives and the latter being the selection of one of the possible options at hand. Session types were first introduced in a variant of the π-calculus to describe binary interactions. Subsequently, they have been extended to multiparty sessions [START_REF] Honda | Multiparty asynchronous session types[END_REF], where several participants interact with each other. In the rest of this paper, we will focus on binary session types.

Session types guarantee privacy and communication safety within a session. Privacy means that session channels are known and used only by the participants involved in the session. Communication safety means that interaction within a session will proceed without mismatches of direction and of message type. To achieve this, a session channel is split into two endpoints, each of which is owned by one of the participants. These endpoints are used according to dual behaviours (and thus have dual types), namely one participant sends what the other one is expecting to receive and vice versa. Indeed, duality is a key concept in the theory of session types.

To better understand session types and the notion of duality, let us consider a simple example: the equality test. A server and a client communicate over a session channel. The endpoints x and y of the session channel are owned by the server and the client, respectively and exclusively, and must have dual types. To guarantee duality of types, static checks are performed by the type system.

If the type of the server endpoint x is S ?Int.?Int.!Bool.end -meaning that the process owning the channel endpoint x receives (?) an integer value followed by another integer value and then sends (!) back a boolean value corresponding to the equality test of the integers received -then the type of the client endpoint y should be S !Int.!Int.?Bool.end -meaning that the process owning the channel endpoint y sends an integer value followed by another integer value and then waits to receive back a boolean value -which is exactly the dual type.

There is a precise moment at which a session between two participants is established. It is the connection phase, when a fresh (private) session channel is created and its endpoints are bound to each communicating process. The connection is also the moment when duality, hence mutual compliance of two session types, is verified. In order to establish a connection, primitives like accept/request or (νxy), are added to the syntax of terms [START_REF] Takeuchi | An Interaction-based Language and its Typing System[END_REF][START_REF] Honda | Language primitives and type disciplines for structured communication-based programming[END_REF][START_REF] Vasco | Fundamentals of session types[END_REF].

When session types and session terms are added to the syntax of standard π-calculus types and terms, respectively, the syntax of types (and, as a consequence, of type environments) usually needs to be split into two separate syntactic categories, one for session types and the other for standard π-calculus types [START_REF] Takeuchi | An Interaction-based Language and its Typing System[END_REF][START_REF] Honda | Language primitives and type disciplines for structured communication-based programming[END_REF][START_REF] Yoshida | Language Primitives and Type Discipline for Structured Communication-Based Programming Revisited: Two Systems for Higher-Order Session Communication[END_REF][START_REF] Gay | Subtyping for session types in the pi calculus[END_REF]. Common typing features, like subtyping, polymorphism, recursion have then to be added to both syntactic categories. Also the syntax of processes will contain both standard πcalculus process constructs and session process constructs (for example, the constructs mentioned above to create session channels). These syntactic redundancies bring in redundancies also in the theory, and can make the proofs of properties of the language heavy. Moreover, if a new type construct is added, the corresponding properties must be checked both on standard π-types and on session types. By "standard type systems" we mean type systems originally studied in depth for sequential languages such as the λcalculus and then transplanted onto the π-calculus as types for channel names (rather than types for terms as in the λ -calculus); they include, for instance, constructs for products, records, variants, polymorphism, linearity, capabilities, and so on.

A further motivation for investigating the expressiveness of the π-calculus with or without session types is the similarity between session constructs and standard π-calculus constructs. Consider the type S = ?Int.?Int.!Bool.end. This type is assigned to a session channel endpoint and it describes a structured sequence of inputs and outputs by specifying the type of messages that the channel can transmit. This way of proceeding reminds us of the linearised channels [START_REF] Kobayashi | Linearity and the pi-calculus[END_REF], which are channels used multiple times for communication but only in a sequential manner. Linearised types can, in turn, be encoded into linear types-i.e., channel types used exactly once [START_REF] Kobayashi | Linearity and the pi-calculus[END_REF]. Similarly, there are analogies between the branch and select constructs of session types and the variant types [START_REF] Sangiorgi | An Interpretation of Typed Objects into Typed pi-Calculus[END_REF][START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF] of standard π-calculus types, as well as between the duality of session types, in which the behaviour of a session channel is split into In this paper we follow the encoding of binary session types into linear π-types from [START_REF] Dardha | Session types revisited[END_REF][START_REF] Dardha | Session types revisited[END_REF], then discuss some extensions and applications. The encoding was first suggested by Kobayashi [33], as a proof-of-concept without however formally studying it. Later, Demangeon and Honda [START_REF] Demangeon | Full Abstraction in a Subtyped pi-Calculus with Linear Types[END_REF] proposed an encoding of session types into π-types with the aim of studying the subtyping relation, and proving properties such as soundness of the encoding with respect to typing and full abstraction.

v ::= x (name) ⋆ (unit value) (R-STNDCOM) x! v .P | x?(z).Q → P | Q[v/z] (R-COM) (νxy)(x! v .P | y?(z).Q) → (νxy)(P | Q[v/z]) (R-CASE) (νxy)(x ⊳ l j .P | y ⊲ {l i : P i } i∈I ) → (νxy)(P | P j ) j ∈ I (R-STNDRES) P → Q =⇒ (νx)P → (νx)Q (R-RES) P → Q =⇒ (νxy)P → (νxy)Q (R-PAR) P → Q =⇒ P | R → Q | R (R-STRUCT) P ≡ P ′ , P → Q, Q ′ ≡ Q =⇒ P ′ → Q ′
Structure of the paper. The rest of the paper is organised as follows. In Section 3 we introduce the necessary background about the session π-calculus and the linear π-calculus. In Section 4 we recall the encoding from the session π-calculus into the linear π-calculus, as well as its correctness result. In Section 5 and Section 6 we discuss respectively some extensions and some applications of the encoding.

Background: π-calculus and session types

In this section, we recall the syntax and semantics of our two calculi of interest: the session π-calculus and the standard typed π-calculus. We also introduce the notion of duality for session types. Session types and terms. The syntax for session types and session π-calculus terms is reported in Figure 1, together with the rules for the reduction semantics, in which ≡ is the usual structural congruence relation, allowing one to rearrange parallel compositions and the scope of restrictions and to remove useless restrictions. We refer to, e.g., [START_REF] Vasco | Fundamentals of session types[END_REF][START_REF] Gay | Subtyping for session types in the pi calculus[END_REF] for the rules for typing. Session types range over S and types range over T ; the latter include session types, standard channel types denoted by ♯T , data types, such as Unit and any other type construct needed for mainstream programming.

P | Q (composition) (νx)P (restriction) case v of {l i (x i ) ⊲ P i } i∈I (case) v ::= x (name) ⋆ (unit value) l v (variant value) (Rπ-COM) x! ṽ .P | x?(z).Q → P | Q[ ṽ/z] (Rπ-CASE) case l j v of {l i (x i ) ⊲ P i } i∈I → P j [v/x j ] j ∈ I (Rπ-RES) P → Q =⇒ (νx)P → (νx)Q (Rπ-PAR) P → Q =⇒ P | R → Q | R (Rπ-STRUCT) P ≡ P ′ , P → Q, Q ′ ≡ Q =⇒ P ′ → Q ′
Session types are: end, the type of a terminated channel; ?T.S and !T.S (used in the equality test example given in the introduction) indicating, respectively, the receive and send of a value of type T , with continuation type S. Branch and select are sets of labelled session types, whose labels have indices ranging over a non-empty set I. Branch &{l i : S i } i∈I indicates an external choice, namely what is offered, and it is a generalisation of the input type in which the continuation S i depends on the received label l i . Dually, select ⊕{l i : S i } i∈I indicates an internal choice, where only one of the available labels l i 's will be chosen, and it is a generalisation of the output type.

Session processes range over P, Q. The output process x! v .P sends a value v on channel endpoint x and continues as P; the input process x?(y).P receives on x a value to substitute for the placeholder y in the continuation P. The selection process x ⊳ l j .P selects label l j on channel x and proceeds as P. The branching process x ⊲ {l i : P i } i∈I offers a range of labelled alternative processes on channel x. The session restriction construct (νxy)P creates a session channel, more precisely its two endpoints x and y, and binds them in P. As usual, the term 0 denotes a terminated process and P | Q the parallel composition of P and Q.

Duality Session type duality is a key ingredient in session types theory as it is necessary for communication safety. Two processes willing to communicate, e.g., the client and the server in the equality test, must first agree on a session protocol. Intuitively, client and server should perform dual operations: when one process sends, the other receives, when one offers, the other chooses. Hence, the dual of an input must be an output, the dual of branch must be a select, and vice versa. Formally, duality on session types is defined as the following function:

end end !T.S ?T.S ?T.S !T.S ⊕{l i : S i } i∈I &{l i : S i } i∈I &{l i : S i } i∈I ⊕{l i : S i } i∈I
The static checks performed by the typing rules make sure that the peer endpoints of the same session channel have dual types. In particular, this is checked in the restriction rule (T-RES) below:

(T-RES) Γ, x : T, y : T ⊢ P Γ ⊢ (νxy)P
Standard π-calculus. The syntax and reduction semantics for the standard π-calculus are shown in Figure 2. We use t to range over standard π-types, to distinguish them from types T and session types S, given in the previous paragraph. We also use the notation • to indicate (finite) sequences of elements. Standard π-types specify the capabilities of channels. The type / 0[] is assigned to a channel without any capability, which cannot be used for any input/output action. Standard types ℓ i [ t] and ℓ o [ t] are assigned to channels used exactly once to receive and to send a sequence of values of type t, respectively. The variant type l i t i i∈I is a labelled form of disjoint union of types t i whose indices range over a set I.

Linear types and variant types are essential in the encoding of session types. The addition of variant types, as of any structured type, implies the addition of a constructor in the grammar for values, to produce variant values of the form l v, and of a destructor in the grammar for processes, to consume variant values. Such a destructor is represented by the term case v of {l i (x i ) ⊲ P i } i∈I , offering different behaviours depending on which variant value l v is received and binding v to the corresponding x i . In the operational semantics, the reduction rule in which a variant value is consumed (Rπ-CASE) is sometimes called case normalisation. Unlike the session π-calculus, the standard π-calculus has just one restriction operator that acts on single names, as in (νx)P.

Encoding sessions

In this section we present the encoding of session π-calculus types and terms into linear π-calculus types and terms, together with the main technical results, following Dardha et al. [START_REF] Dardha | Session types revisited[END_REF][START_REF] Dardha | Session types revisited[END_REF].

Type encoding. The encoding of session types into linear π-types is shown at the top of Figure 3. Types produced by grammar T are encoded in a homomorphic way, e.g., ♯T ♯ T . The encoding of end is a channel with no capabilities / 0[] that cannot be used further. Type ?T.S is encoded as the linear input channel type carrying a pair of values whose types are the encodings of T and of S. The encoding of !T.S is similar except that the type of the second component of the pair is the encoding of S, since it describes the type of a channel as it will be used by the receiver process. The branch and the select types are encoded as linear input and linear output channels carrying variant types having labels l i and types that are respectively the encoding of S i and the encoding of S i for all i ∈ I. Again, the reason for using duality of the continuation in the encoding of the select type is the same as for the output type, as select is a generalisation of output type.

end / 0[] (E-END) !T.S ℓ o [ T , S ] (E-OUT) ?T.S ℓ i [ T , S ] (E-INP) ⊕{l i : S i } i∈I ℓ o [ l i S i i∈I ] (E-SELECT) &{l i : S i } i∈I ℓ i [ l i S i i∈I ] (E-BRANCH) x f f x (E-NAME) ⋆ f ⋆ (E-STAR) 0 f 0 (E-INACTION) x! v .P f (νc) f x ! v f , c . P f {x →c} (E-OUTPUT) x?(y).P f f x ?(y, c). P f {x →c} (E-INPUT) x ⊳ l j .P f (νc) f x ! l j c . P f {x →c} (E-SELECTION) x ⊲ {l i : P i } i∈I f f x ?(y). case y of {l i (c) ⊲ P i f {x →c} } i∈I (E-BRANCHING) P | Q f P f | Q f (E-COMPOSITION) (νxy)P f (νc) P f {x,y →c} (E-RESTRICTION) (νx)P f (νx) P f (E-NEW)
Process encoding. The encoding of session processes into standard π-processes is shown at the bottom of Figure 3. The encoding of a process P is parametrised by a function f from channel names to channel names. We say that f is a renaming function for P if, for all the names x that occur free in P, either f (x) = x or f (x) is a fresh name not occurring in n(P), where n(P) is the set of all names of P, both free and bound. Also, f is the identity function on all bound names of P. Hereafter we write dom( f ) for the domain of f and f x as an abbreviation for f (x). During the encoding of a session process, its renaming function f is progressively updated. For example, we write f {x → c} or f {x, y → c} for the update of f such that the names x and y are associated to c. The notion of a renaming function is extended also to values as expected. In the uses of the definition of the renaming function f for P (respectively v), process P (respectively value v) will be typed in a typing context, say Γ. It is implicitly assumed that the fresh names used by f (that is, the names y such that y = f (x), for some x = y) are also fresh for Γ.

The motivation for parametrising the encoding of processes and values with a renaming function stems from the key idea of encoding a structured communication over a session channel as a chain of one-shot communications over linear channels. Whenever we transmit some payload on a linear channel, the payload is paired with a fresh continuation channel on which the rest of the communication takes place. Such continuation, being fresh, is different from the original channel. Thus, the renaming function allows us to keep track of this fresh name after each communication.

We now provide some more details on the encoding of terms. Values are encoded as expected, so that a channel name x is encoded to f x and the ⋆ unit value is encoded to itself. This encoding is trivially extended to every ground value added to the language. In the encoding of the output process, a new channel name c is created and is sent together with the encoding of the payload v along the channel f x . The encoding of the continuation process P is parametrised by an updated f where the name x is associated to c. Similarly, the input process listens on channel f x and receives a pair whose first element (the payload) replaces the name y and whose second element (the continuation channel c) replaces x in the continuation process by means of the updated renaming function f {x → c}. As indicated in Section 3, session restriction (νxy)P creates two fresh names and binds them in P as the opposite endpoints of the same session channel. This is not needed in the standard π-calculus. The restriction construct (νx)P creates and binds a unique name x in P; this name identifies both endpoints of the communicating channel. The encoding of a session restriction process (νxy)P is a standard channel restriction process (νc) P f {x,y →c} with the new name c used to substitute both x and y in the encoding of P. Selection x ⊳ l j .P is encoded as the process that first creates a new channel c and then sends on f x a variant value l j c, where l j is the selected label and c is the channel created to be used for the continuation of the session. The encoding of branching receives on f x a value, typically being a variant value, which is the guard of the case process. According to the transmitted label, one of the corresponding processes P i f {x →c} for i ∈ I will be chosen. Note that the name c is bound in any process P i f {x →c} . The encoding of the other process constructs, namely inaction, standard channel restriction, and parallel composition, acts as a homomorphism.

Example 4.1 (Equality test). We illustrate the encoding of session types and terms on the equality test from the introduction. Thus we also make use of boolean and integer values, and simple operations on them, whose addition to the encoding is straightforward.

The encoding of the server's session type S is

S = ℓ i [Int, ℓ i [Int, ℓ o [Bool, / 0[]]]]
while that of the client's session type S is

S = ℓ o [Int, ℓ i [Int, ℓ o [Bool, / 0[]]]]
Note how the encoding of dual session types boils down to linear channel types that have the same payload and dual outermost capabilities ℓ i [•] and ℓ o [•]. This property holds in general and can be exploited to express the (complex) notion of session type duality in terms of the (simple) property of type equality, as we will see in Section 6.

The server process, communicating on endpoint x of type S, is server x?(z 1 ).x?(z 2 ).x! z 1 == z 2 .0 and the client process, communicating on endpoint y of type S, is client y! 3 .y! 5 .y?(eq).0

Then we have server {x →s} = s?(z 1 , c). x?(z 2 ).x! z 1 == z 2 .0 {x →c}

= s?(z 1 , c).c?(z 2 , c ′ ).(νc ′′ )c ′ ! z 1 == z 2 , c ′′ .0

EXPRESSing Session Types

Similarly, client {y →s} = (νc)s! 3, c .(ν c ′ )c! 5, c ′ .c ′ ?(eq, c ′′ ).0

The whole server-client system is thus encoded as follows, using / 0 for the identity function.

(νxy)(server | client) / 0 = (νs) (server | client) {x,y →s} = (νs) server {x →s} | client {y →s} (The update {x, y → s} reduces to {x → s} on the server and to {y → s} on the client because they do not contain occurrences of y and x respectively.)

Correctness of the encoding. The presented encoding can be considered as a semantics of session types and session terms. The following theoretical results show that indeed we can derive the typing judgements and the properties of the π-calculus with sessions via the encoding and the corresponding properties of the linear π-calculus.

First, the correctness of an encoded typing judgement on the target terms implies the correctness of the judgement on the source terms, and conversely. Similar results hold for values. The encoding is extended to session typing contexts in the expected manner. Theorem 4.2 (Type correctness). The following properties hold:

1. If Γ ⊢ P, then Γ f ⊢ P f for some renaming function f for P;

2. If Γ f ⊢ P f for some renaming function f for P, then Γ ⊢ P. Theorem 4.2, and more precisely its proof [START_REF] Dardha | Session types revisited[END_REF][START_REF] Dardha | Type Systems for Distributed Programs: Components and Sessions[END_REF], shows that the encoding can be actually used to reconstruct the typing rules of session types. That is, the typing rules for an operator op of the session π-calculus can be 'read back' from the typing of the encoding of op.

Next we recall the operational correctness of the encoding. That is, the property that the encoding allows one to faithfully reconstruct the behaviour of a source term from that of the corresponding target term. We recall that → is the reduction relation of the two calculi. We write ֒→ for the extension of the structural congruence ≡ with a case normalisation indicating the decomposition of a variant value (Section 3). Theorem 4.3 (Operational correspondence). Let P be a session process, Γ a session typing context, and f a renaming function for P such that Γ f ⊢ P f . Then the following statements hold.

1. If P → P ′ , then P f →֒→ P ′ f . 2. If P f → Q, then there is a session process P ′ such that

• either P → P ′ ;

• or there are x and y such that (νxy)P → P ′ and Q ֒→ P ′ f . Statement 1 of the above theorem tells us that the reduction of an encoded process mimics faithfully the reduction of the source process, modulo structural congruence or case normalisation. Statement 2 of the theorem tells us that if the encoding of a process P reduces to the encoding of a process P ′ (via some intermediate process Q), then the source process P will reduce directly to P ′ or it might need a wrap-up under restriction. The reason for the latter is that in the session π-calculus [START_REF] Vasco | Fundamentals of session types[END_REF], reduction only occurs under restriction and cannot occur along free names. In particular, in the theorem, f is a generic renaming function; this function could map two free names, say x and y, onto the same name; in this case, an input at x and an output at y in the source process could not produce a reduction, whereas they might in the target process.

The two theorems above allow us to derive, as a straightforward corollary, the subject reduction property for the session calculus. Other properties of the session π-calculus can be similarly derived from corresponding properties of the standard π-calculus. For instance, since the encoding respects structural congruence (that is, P ≡ P ′ if and only if P f ≡ P ′ f ), we can derive the invariance of typing under structural congruence in the session π-calculus.

Extensions

In this section we discuss several extensions for the presented encoding, which have been proposed in order to accommodate the additional features of subtyping, polymorphism, recursion, higher-order communication and multiparty interactions.

Subtyping. Subtyping is a relation between types based on a notion of substitutability. If T is a subtype of T ′ , then any channel of type T can be safely used in a context where a channel of type T ′ is expected. In the standard π-calculus, subtyping originates from capability types -the possibility of distinguishing the input and output usage of channels [START_REF] Benjamin | Typing and Subtyping for Mobile Processes[END_REF][START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF]. (This is analogous to what happens in languages with references, where capabilities are represented by the read and write usages.) Precisely, the input channel capability is co-variant, whereas the output channel capability is contra-variant in the types of values transmitted (the use of capabilities is actually necessary with linear types, as reported in Figure 2). Subtyping can then be enhanced by means of the variant types, which are co-variant both in depth and in breadth. In the case of session π-calculus, subtyping must be dealt with also at the level of session types [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF]; for instance, branch and select are both co-variant in depth, whereas they are co-variant and contra-variant in breadth, respectively. This duplication of effort can become heavy, particularly when types are enriched with other constructs (a good example are recursive types). The encoding of session types naturally accommodates subtyping, indeed subtyping of the standard π-calculus can be used to derive subtyping on session types. Writing <: and ≤ for, respectively, subtyping for session types and for standard π-types, for instance we have: Theorem 5.1 (Encoding for Subtyping). T <: T ′ if and only if T ≤ T ′ .

Polymorphism and Higher-Order Communication. Polymorphism is a common and useful type abstraction in programming languages, as it allows operations that are generic by using an expression with several types. Parametric polymorphism has been studied in the standard π-calculus [START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF], and in the π-calculus with session types [START_REF] Caires | Behavioral Polymorphism and Parametricity in Session-Based Communication[END_REF]; for bounded polymorphism in session π-calculus see Gay [START_REF] Gay | Bounded polymorphism in session types[END_REF].

The Higher-Order π-calculus (HOπ) models mobility of processes that can be sent and received and thus can be run locally [START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF]. Higher-order communication for the session π-calculus [START_REF] Mostrous | Two Session Typing Systems for Higher-Order Mobile Processes[END_REF] has the same benefits as for the π-calculus, in particular, it models code mobility in a distributed scenario.

Extensions of the encoding to support polymorphism and HOπ have been studied in [START_REF] Dardha | Session types revisited[END_REF][START_REF] Dardha | Session types revisited[END_REF][START_REF] Dardha | Type Systems for Distributed Programs: Components and Sessions[END_REF] and used to test its robustness. The syntax of types and terms is extended to accommodate the new constructs. For polymorphism, session types and standard π-types are extended with a type variable X and with polymorphic types X ; T and X ;t , respectively. For higher-order communication, session types and standard π-types are extended with the functional type T → σ , assigned to a functional term that can be used without any restriction, and with the linear functional type T 1 → σ that must be used exactly once. Correspondingly, the syntax of processes is extended to accommodate the unpacking process (open v as (X ; x) in P) to deal with polymorphism, and with call-by-value λ -calculus primitives, namely abstraction (λ x : T.P) and application (PQ), to deal with higher-order communication.

The encoding of the new type and process constructs is a homomorphism in all cases. Consequently, the proof cases added to Theorems 4.2 and 4.3 are trivial.

Recursion. The encoding was also extended to accommodate recursive types and replicated processes by Dardha [START_REF] Dardha | Recursive Session Types Revisited[END_REF]. Here, the new added types are a recursive type µX .T and a type variable X , as well as the replicated process * P. Recursive (session) types are required to be guarded, meaning that in µX .T , variable X may occur free in T only under at least one of the other type constructs. The paper uses a new duality function, called complement, which is inspired by the work of Bernardi et al. [START_REF] Bernardi | Using Higher-Order Contracts to Model Session Types (Extended Abstract)[END_REF][START_REF] Bernardi | On Duality Relations for Session Types[END_REF]. Some new cases for the encoding of recursive session types and processes are:

X X µX .S µX . S * P f * P f
The extended encoding is proved to be sound and complete with respect to typing and reduction (aka operational correspondence). We refer the interested reader to [START_REF] Dardha | Recursive Session Types Revisited[END_REF][START_REF] Dardha | Recursive Session Types Revisited[END_REF].

Multiparty Session Types. Multiparty Session Types (MPSTs) [START_REF] Honda | Multiparty asynchronous session types[END_REF][START_REF] Honda | Multiparty asynchronous session types[END_REF] accommodate communications between more than two participants. Since their introduction, they have become a major area of investigation within the session type community. Their meta-theory is more complex than that of the binary case, and it is beyond the scope of this paper to revise it in detail. The core syntax of multiparty session types is given by the following grammar where selection and branching types are annotated with roles identifying the participant of a multiparty session to which a message is sent or from which a message is expected. The message consists of a label l i and a payload of type U i , whereas the continuation S i indicates how the session endpoint is meant to be used afterwards.

A multiparty session type describes the behaviour of a participant of a multiparty session with respect to all the other participants it interacts with, identified by their role in the session type. In order to obtain the behaviour of a participant with respect to another particular participant of the multiparty session, say q, the multiparty session type must be projected onto q. Hereafter, we write S ↾ q for the partial projection of S onto q, referring to [START_REF] Scalas | A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming[END_REF][START_REF] Scalas | A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming[END_REF] for its precise definition. Projection yields a type defined by the following syntax, which resembles that of binary session types:

H ::= end | X | µX .H (termination, type variable, recursive type) ⊕ i∈I !l i (U i ).H i (select) & i∈I ?l i (U i ).H i (branch)
Projection is a key feature of MPSTs as it is needed in the technical development of a sound type system. At the same time, it also provides a hook by which multiparty sessions and multiparty session types can be encoded in the standard π-calculus through the encoding of (binary) session types that we have outlined in Section 3.

Let us briefly comment on the encoding of MPST into linear types given by Scalas et al. [START_REF] Scalas | A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming[END_REF][START_REF] Scalas | A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming[END_REF]. This encoding is fully fledged as it covers the whole MPST and it preserves the theory's distributivity. Previous work by Caires and Pérez [START_REF] Caires | Multiparty Session Types Within a Canonical Binary Theory, and Beyond[END_REF] presents an encoding of MPST into binary session types via a medium process, which acts as an orchestrator for the encoding, thus losing distributivity. In the encoding of Scalas et al. no orchestrator is used, hence the encoding preserves its intended choreographic nature as opposed to being orchestrated.

The encoding of a multiparty session type from Scalas et al. is formally defined as:

S [p : S ↾ p ] p∈S
resulting in a record of types with an entry for each role p occurring in the multiparty session type S.

The encoding of a projected type, namely S ↾ p , can then be obtained by suitably adapting the function defined in Figure 3. The main cases are summarised below, and the encoding is a homomorphism for the other constructs in the syntactic category H presented above.

⊕ i∈I !l i (U i ).H i ℓ o [ l i ( U i , H i ) i∈I ] & i∈I ?l i (U i ).H i ℓ i [ l i ( U i , H i ) i∈I ]
The encoding of processes is quite complex and beyond the scope of this paper. The interested reader may refer to Scalas et al. [START_REF] Scalas | A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming[END_REF][START_REF] Scalas | A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming (Artifact)[END_REF] for the formal details and a Scala implementation of multiparty sessions based on this encoding. The encoding of MPST into linear types satisfies several properties, including duality and subtyping preservation, correctness of the encoding with respect to typing, operational correspondence and deadlock freedom preservation. These properties are given in Section 6 of [START_REF] Scalas | A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming[END_REF].

Applications

The encoding from session types to linear channel types can be thought of as a way of "explaining" a high-level type language in terms of a simpler, lower-level type language. Protocols written in the lowerlevel type language tend to be more cumbersome and less readable than the session types they encode. For this reason, it is natural to think of the encoding as nothing more than a theoretical study. Yet, as we are about to see in this section, the very same encoding has also enabled (or at least inspired) further advancements in the theory and practice of session types.

A Type System for Deadlock Freedom

A well-typed session π-calculus process (and equivalently a well-typed standard π-calculus one) enjoys communication safety (no message with unexpected type is ever exchanged) but not deadlock freedom. For example, both the session π-calculus process (νx 1 x 2 )(νy 1 y 2 ) (x 1 ?(z).y 1 ! z .0 | y 2 ?(w).x 2 ! w .0)

and the standard π-calculus process (νx)(νy) (x?().y! .0 | y?().x! .0)

are well-typed in the respective typing disciplines, but the behaviours they describe on the two sessions/channels are intermingled in such a way that no communication can actually occur: the input from each session/channel must be completed in order to perform the output on the other session/channel. Several type systems that ensure deadlock freedom in addition to communication safety have been studied for session and standard typed π-calculi. In a particular line of work, Kobayashi [START_REF] Kobayashi | A Type System for Lock-Free Processes[END_REF][START_REF] Kobayashi | A New Type System for Deadlock-Free Processes[END_REF] has studied a typing discipline that associates priorities to channel types so as to express, at the type level, the relative order in which channels are used, thus enabling the detection of circular dependencies, such as the one shown above. Later on, Padovani [START_REF] Padovani | Deadlock and lock freedom in the linear π-calculus[END_REF] has specialised this technique for the linear π-calculus and, as an effect of the encoding illustrated in Section 3, for the session π-calculus as well. To illustrate the technique, in this section we consider a refinement of the linear input/output types in Figure 2 as follows t :

:= ℓ o [ t ] m | ℓ i [ t ] n | • • •
where m and n are integers representing priorities: the smaller the number, the higher the priority with which the channel must be used. In the process (2) above, we could assign the types ℓ i [] m and ℓ o [] n to respectively x and y on the lhs of | and the types ℓ o [] m and ℓ i [] n to respectively x and y on the rhs of |. Note that each channel is assigned two types having dual polarities (each channel is used in complementary ways on the two sides of |) and the same priority. Then, the type system imposes constraints on priorities to reflect the order in which channels are used: on the lhs of | we have the constraint m < n since the input on x (with priority m) blocks the output on y (with priority n); on the rhs of | the opposite happens, resulting in the constraint n < m. Obviously, these two constraints are not simultaneously satisfiable, hence the process as a whole is ruled out as ill typed.

In such simple form, this technique fails to deal with most recursive processes. We illustrate the issue through the following server process that computes the factorial of a natural number, in which we use a few standard extensions (replication, conditional, numbers and their operations) to the calculus introduced earlier. * fact?(x, y).if x = 0 then y! 1 else (νz

) (fact! x -1, z | z?(k).y! x × k ) (3)
The server accepts requests on a shared channel fact. Each request carries a natural number x and a linear channel y on which the factorial of x is sent as response. The modelling follows the standard recursive definition of the factorial function. In particular, in the recursive case a fresh linear channel z is created from which the factorial k of x -1 is received. At that point, the factorial x × k of x can be sent on y. Now assume, for the sake of illustration, that m and n are the priorities associated with y and z, respectively. Since z is used in the same position as y in the recursive invocation of fact, we expect that z and y should have the same type hence the same priority m = n. This clashes with the input on z that blocks the output on y, requiring n < m. The key observation we can make in order to come up with a more flexible handling of priorities is that a replicated process like (3) above cannot have any free linear channel. In fact, the only free channel fact is a shared one whereas y is received by the process and z is created within the process. As a consequence, the absolute value of the priorities m and n we associate with y and z does not matter (as long as they satisfy the constraint n < m) and they can vary from one request to another. In more technical terms, this corresponds to making fact polymorphic in the priority of the channel y received from it and allowing a (priority-limited) form of polymorphic recursion when we type outputs such as fact! x -1, z .

It must be pointed out that a process such as (3) is in the scope of Kobayashi's type systems [START_REF] Kobayashi | A New Type System for Deadlock-Free Processes[END_REF]. The additional expressiveness resulting from priority polymorphism enables the successful analysis of recursive processes that interleave actions on different linear channels also in cyclic network topologies. We do not showcase these more complex scenarios in this brief survey, instead referring the interested reader to [START_REF] Padovani | Deadlock and lock freedom in the linear π-calculus[END_REF] for an exhaustive presentation of the technique and to [START_REF] Padovani | Type-Based Analysis of Linear Communications[END_REF] for a proof-of-concept implementation.

As a final remark, it is interesting to note that this technique can be retrofitted to a calculus with native sessions, but it was born in the context of the standard π-calculus, which features a more primitive communication model. The point is that, in the standard π-calculus, sequential communications are encoded in a continuation-passing style, meaning that higher-order channels are the norm rather than the exception. So, the quest for expressive type systems ensuring (dead)lock freedom in the standard π-calculus could not ignore this feature, and this necessity has been a major source of inspiration for the support of priority polymorphism. In this direction, Carbone et al. [START_REF] Carbone | Progress as Compositional Lock-Freedom[END_REF] study (dead)lock freedom for session π-processes using the encoding from Section 4 and the technique from [START_REF] Kobayashi | A New Type System for Deadlock-Free Processes[END_REF] and show that this combined technique is more fine-grained than other ones adopted in session Dardha and Pérez [START_REF] Dardha | Comparing type systems for deadlock freedom[END_REF] present a full account of the deadlock freedom property in session π-calculi, and compare deadlock freedom obtained by using the encoding and the work from [START_REF] Kobayashi | A New Type System for Deadlock-Free Processes[END_REF] to linear logic approaches, which are used as a yardstick for deadlock freedom.

Session Type Inference

A major concern regarding all type systems is their realisability and applicability in real-world programming languages. In this respect, session type systems pose at least three peculiar challenges: (1) the fact that session endpoints must be treated as linear resources that cannot be duplicated or discarded; (2) the need to update the session type associated with a session endpoint each time the endpoint is used;

(3) the need to express session type duality constraints in addition to the usual type equality constraints. The first challenge can be easily dealt with only in those (few) languages that provide native support for linear (or at least affine) types. Alternatively, it is possible to devise mechanisms that detect linearity (or affinity) violations at runtime with a modest overhead. The second challenge can be elegantly addressed by adopting a functional API for sessions [START_REF] Gay | Linear type theory for asynchronous session types[END_REF], whereby each function/method using a session endpoint returns (possibly along with other results) the same endpoint with its type suitably updated. The last challenge, which is the focus of this section, is a subtle one since session type duality is a complex relation that involves the whole structure of two session types. In fact, it has taken quite some time even just to correctly define duality in the presence of recursive session types [START_REF] Bernardi | Using Higher-Order Contracts to Model Session Types (Extended Abstract)[END_REF][START_REF] Gay | Duality of Session Types: The Final Cut[END_REF].

Somewhat surprisingly, the encoding of session types into linear channel types allows us to cope with this challenge in the most straightforward way, simply by getting rid of it. In Example 4.1 we have shown two session types, one dual of the other, whose respective encodings are equal except for the outermost capabilities. This property holds in general. In fact, it is possible to devise a slightly different representation of capabilities so that (session) type duality can be expressed solely in terms of type equality. To this aim, let • and • be any two types which we use to represent the absence and presence of a given capability, respectively. We do not need any particular property of • and • except the fact that they must be different. In fact, they need not even be inhabited. Now, we can devise a slightly different syntax for linear channel types, as follows:

t ::= ℓ κ,κ [ t ] | • • • κ ::= • | •
The idea is that a linear channel type carries two separate input and output capabilities (hereafter ranged over by κ and ι), each of which can be either present or absent. For example, ℓ With this representation of linear channel types the dual of a type can be defined simply as ℓ κ,ι [ t ] = ℓ ι,κ [ t ], where the input/output capabilities are swapped. Now, suppose that we wish to express a duality constraint S = T stating that S is the dual of T and let ℓ κ,ι [ s ] = S and ℓ κ ′ ,ι ′ [ t ] = T be the encodings of S and T , respectively. Using Proposition 6.1 and the revised representation of linear channel types we obtain S = T ⇐⇒ κ = ι ′ ∧ ι = κ ′ ∧ s = t thereby turning a session type duality constraint into a conjunction of type equality constraints.

This apparently marginal consequence of using encoded (as opposed to native) session types makes it possible to rely on completely standard features of conventional type systems to express and infer complex structural relations on session types. In particular, it allows any Hindley-Milner type inference algorithm to perform session type inference. FuSe [START_REF] Padovani | Type-Based Analysis of Linear Communications[END_REF] is a library implementation of session types for OCaml that showcases this idea at work. The library supports higher-order sessions, recursive session types and session subtyping by piggybacking on OCaml's type system. Clearly, the inferred (encoded) session types are not as readable as the native ones. This may pose problems in the presence of type errors. To address this issue, the library is accompanied by an external tool called Rosetta that decodes encoded session types and pretty prints them as native ones using the inverse of the encoding function

• . 1 On similar lines, Scalas and Yoshida [START_REF] Scalas | Lightweight Session Programming in Scala[END_REF] develop lchannels, a Scala library for session types fully based on the encoding of session types into linear types. As a result, the structure of a session type is checked statically by analysing its encoding onto channel types in Scala, while linearity is checked dynamically at run time as in FuSe, as Scala has no support for linearity.

Figure 1 :

 1 Figure 1: Syntax and reduction semantics of the session π-calculus

Figure 2 :

 2 Figure 2: Syntax and reduction rules of the standard typed π-calculus

Figure 3 :

 3 Figure 3: Encoding of types, values and processes.

Corollary 4 . 4 (

 44 Session Subject Reduction). If Γ ⊢ P and P → Q, then Γ ⊢ Q.

Corollary 4 . 5 (

 45 Session Structural Congruence). If Γ ⊢ P and P ≡ P ′ , then also Γ ⊢ P ′ .

S

  ::= end | X | µX .S (termination, type variable, recursive type) p⊕ i∈I !l i (U i ).S i (select towards role p) p& i∈I ?l i (U i ).S i (branch from role p) B ::= Unit | . . . (base type) U ::= B | S (closed under µ) (payload type)

Proposition 6 . 1 .

 61 Let • be the partial involution on types such that/ 0[] = / 0[] and ℓ i [ t ] = ℓ o [ t ] and ℓ o [ t ] = ℓ i [ t ].Then S = S for every S.

  •,• [] would be EXPRESSing Session Types the same as / 0[], ℓ •,• [ t ] would be the same as ℓ i [ t ] and ℓ •,• [ t ] would be the same as ℓ o [ t ].

The source code of FuSe and Rosetta is publicly available at https://github.com/boystrange/FuSe.