A Gentle Introduction to Session Types

(1)

Pekka Peltola

A GENTLE INTRODUCTION TO SESSION TYPES

Faculty of Information Technology and Communication Sciences Master’s Thesis

(2)

ABSTRACT

Pekka Peltola: A Gentle Introduction to Session Types Master’s Thesis

Tampere University Computer Science June 2021

We present session types, a type formalism for structured communication. The goal of the thesis is to give an elementary introduction to session types for a new reader with only a little or no knowledge of related concepts, such as π-calculus or type systems. We start by motivating the reader with an informal example and later define the language formally. Only basic language constructs are defined at the beginning and the language is extended gradually. We prove the soundness of the type system, give practical example how session types help developing server- client systems and finally talk briefly about extensions and related work.

Keywords: type systems, session types, pi-calculus, concurrency, processes

(3)

1 Introduction

In concurrent and distributed systems, for example server-client systems, interaction partners communicate on an agreed protocol. The protocol describes the type and direction of the exchanged data. Session types, first proposed almost thirty years ago by Honda [1] and later revised by Takeuchi et al. [2] and Honda et al. [3], are a type formalism to model such interactions. They allow describing protocols as types and verifying the conformance of an implementation by static typechecking.

Session types have been mostly developed using Milner’s π-calculus [4] as a framework. The original work used a variant of π-calculus and later session types and session primitives were added to the standardπ-calculus [5] by Gay and Hole. Many extensions to session types have been studied, such as subtyping [5], multiparty session types [6] and polymorphism [7]. In [8] Kobayashi presented an encoding of session types to standardπ-calculus with types, which was further studied by Dardha et al. [9].

A session is a unit of abstraction for describing information exchange between two interacting partners. Whenever a new session is established, a fresh channel, asession channel, is created, and all communication in the session is done privately via the session channel. A session type is used to describe one end of a session channel and the other end has a dual type. Duality guarantees communication safety, namely that the types of received and sent messages match, andcommunication fidelity, namely that the structure of the messages is as expected.

A session type consists of a sequence of input and output operations, together with external and internal choices, namely the offering of options and the selection of an option, respectively. Let us consider session types

S₁ := ?string.!int.end,

S2 := ?string.?string.!string.endand S := &hlength:S₁,concat:S₂i.

The first one describes a process that receives a string and sends back an integer, the second one receives two strings and sends back a string and the last one gives options, namely ’length’ and ’concat’, and behaves as described byS₁ orS₂ depending on the choice. Thus,Scould describe a server that gives the length of a string or concatenates two strings, when a client selects ’length’

(5)

or ’concat’, respectively. A client communicating with the server should have a dual type, that is,

C₁ := !string.?int.end,

C₂ := !string.!string.?string.endand C :=⊕hlength:C₁,concat:C₂i.

We introduce basics ofπ-calculus and do not assume the reader to have prior knowledge of the calculus. However, we encourage the reader to refer to books by Milner [10] and Sangiorgi and Walker [11] for more information. Similarly, we introduce basics to understand the typing rules and derivations we use. About type systems in general and about types for π-calculus the reader can refer to [12] and [11], respectively. A reader familiar with (simply typed) λ-calculus [13]

will find many of the concepts familiar. We assume the reader to know basics of university level mathematics.

The goal of this thesis is to give a solid basis for understanding session types.

We are not trying to give an overview nor dive too deep in the theory, but show the very basics in great detail. Our goal is to

1. give a clear introduction toπ-calculus and session types for a new reader, 2. combine syntax and rules from multiple sources to create a language, which is easy to approach and clearly distinguishes standard channels and session channels,

3. show detailed examples and proofs to reduce the reader’s learning curve.

We begin Section 2 with an informal example to familiarise the reader with the concepts of the theory. In Section 3 we give syntax for process terms and define operational semantics. In Section 4 we give syntax for types and define typing rules. The soundness of the type system is proved in Section 5. After formal theory sections we give a practical example in Section 6 to demonstrate the power of session types for any developer. We briefly discuss extensions and related work in Section 7.

(6)

2 Session types informally

In this section we give an example from the literature of session types. The language used is formally defined in the next sections. For illustration purposes the language in this section is extended with data values and data types, and statements such as if-then-else.

The example, an automated teller machine (ATM), was presented in [3] and is used in many works, for example in [14] by Dezani-Ciancaglini and de’Liguoro and in [15] by H ¨uttel et al. Consider an ATM, which requests for an identifier from the user and then gives three options to choose from: deposit, withdraw and balance. If the user deposits money, the ATM asks for an amount and sends back the new balance. If the user withdraws, the ATM asks for an amount and either sends back that amount of money (dispense) or notifies that an overdraft oc- curred. If user selects balance, the ATM simply sends back the current balance.

Session type for the ATM is

S := ?string.&hdeposit:S_dep,withdraw :S_wd,balance:S_bali, S_dep:= ?int.!int.end,

Swd := ?int.⊕ hdispense:!int.end,overdraft:!string.endi, S_bal :=!int.end.

Here!denotes receiving,? sending,&offering and finally⊕selection. Further- more, a dot denotes sequencing. Similarly to the example in the introduction, the user using the ATM should have a dual type, which can be obtained by replacing

!with?and&with⊕. Session type for the user is then

C := !string.⊕ hdeposit:C_dep,withdraw :C_wd,balance:C_bali, C_dep:= !int.?int.end,

C_wd:= !int.&hdispense:?int.end,overdraft:?string.endi, C_bal:=?int.end.

We now have a protocol for the communication between the ATM and the user.

Next we need process implementations conforming with it. Aπ-calculus process

(7)

implementing the ATM is

AT M :=a?(z).z?(id).z .{deposit:AT Mdep

withdraw:AT M_wd balance:AT M_bal} AT Mdep :=z?(amount).z!hamount+curr bali.0

AT M_wd :=z?(amount).[ifamount > curr bal]z /overdraft.z!h’ERR’i.0 [else]z /dispense.z!hamounti.0

AT M_bal:= z!hcurr bali.0.

Above x?(y) denotes receiving via x and replacing y with the received value.

x!hyi denotes sending value yvia x. Further, x .{. . .}and x / . . . denote offering and selection, respectively. Value curr bal denotes the current balance for the user. The ATM receives one end of a session channel via channel a and uses the received channel to communicate with the user. Note that the type of values a session channel is capable of sending or receiving changes during the communication.

A process implementing a user depositing money is

U ser:= (υxy) (a!hyi.x!h⁰identif ier⁰i.x /deposit.U ser_dep) U serdep:= x!hamounti.x?(newbalance).0.

The user creates and restricts ((υxy) . . .) two ends of a session channel and sends the other end,y, to the ATM viaa. Restriction guarantees that the communication occurs privately. Then, the user sends his/her identifier and chooses to deposit money. Finally the user sends the amount to deposit and receives the new balance.

(8)

3 Processes

Before presenting the main topic, session types, we need a programming language for processes, which is extended with types later. We start from the very basics, define and explain the language carefully and show examples, how processes can interact. We proceed slowly starting from basic constructs and extend the language gradually. First we present the syntax (of a subset) of standard π-calculus together with operational semantics. We omit sum, name matching and silent action, as is common in the literature of session types. Later, in section 3.3, we add session primitives. For simplicity we use monadic π- calculus. For more details on the theory in sections 3.1 and 3.2 the reader can refer to [11, pp. 11-36].

3.1 Syntax

Terms in π-calculus are processes, which express mobile systems. Processes can interact by exchanging messages on a channel.

We assume a countably-infinite set N of names, which can be thought of as channel names. Elements of the set N are denoted by lower case letters, usuallyx, y, z, u, v, w.

Definition 3.1. (π-calculus)Theprocessesof the π-calculus are given by syntax

P ::= P |P⁰ (composition)

(υx)P (scope restriction)

∗P (replication)

0 (inaction)

x?(y).P (input)

x!hyi.P (output)

We use P, Q, R to range over processes. We call x?(y) and x!hyi prefixes and say that processesx?(y).P andx!hyi.P areprefixed at namex.

In examples we sometimes use meaningful words for processes and names, such asServer, Client, port, thread, etc. However, this is only to make examples cleaner and more illustrative by splitting the processes in parts. For example we do not accept recursive process definitions such asServer:= Server|P.

(9)

An occurrence of a name or an occurence of a process in a process is defined intuitively. A subterm or subprocess Q of a process P is an occurrence of a process Q in P. For example there are three occurrences of x and one occurrence of x?(y).0 in process R := x!hyi.(υx) (x?(y).0). Subprocesses of R areR,(υx) (x?(y).0),x?(y).0and0.

Next we give a short description on how different process forms are meant to be interpreted.

• An inaction 0 denotes a terminated process, that is, a process that does nothing.

• Anoutput prefix x!hyi.P denotes a process that waits to send the namey viaxand continues behaving asP.

• Aninput prefix x?(y).P denotes a process that waits to receive any name viaxand continues behaving asP withyas a placeholder for the received name.

• A composition P |P⁰ denotes a process consisting of two subprocesses proceeding in parallel. Furthermore, P and P⁰ can interact via shared names. We callP, P⁰ components ofP |P⁰.

• A restriction (υx)P denotes a process, where name x is restricted to P. Subprocesses of P are able to use x to interact, but other processes can not send or receive messages viax.

• Areplication∗P denotes an infinite compositionP |P | · · ·.

Note. We use parentheses for readability. When parentheses are missing, composition has the weakest precedence, others having the same. For example

• (υx)x!hyi.0|0= ((υx) (x!hyi.0))|0

• ∗x?(y).0|x!hui.0 =(∗(x?(y).0))|x!hui.0.

Example 3.2. Process x?(y).u?(v).v!hyi.0 first receives a name via x, then another name via u and finally sends the first received name via the second received name.

ProcessP₁ := x?(y).y!hzi.0|x!hui.0can evolve in three different ways:

1. receive a name viax(, withyas a placeholder), 2. send name uviaxor

(10)

3. interact locally via shared namex.

ProcessP2 := (υx)P1 has only one way to evolve, that is, interacting locally via shared namex. In both processesP₁ andP₂ the components of the process share the namexand, thus, can interact via it.

A process of the form ∗x?(y).P can be thought of as a server waiting on channel x. Whenever a client sends a name, say z, via x, the server creates a new copy of P, where y is replaced by z. Consider processes Server :=

∗x?(y).y!hvi.0andClient:=x!hzi.z?(w).0. Clientsends namez viaxtoServer and Server creates Copy := z!hvi.0. Then Copy sends name v via received name z to Client and both processes terminate. Server continues waiting on channelx.

Note the difference in processesP₁ andP₂ in Example 3.2; P₂ can not send or receive viax, becausexis restricted.

Definition 3.3. We say thatyisbinding withscopeP in processesx?(y).P and (υy)P. An occurrence of a name, sayy, isbound, if it is a binding occurrence or it lies within the scope of a binding occurrencey. If an occurrence is not bound, we say it isfree. We writefn(P)for set of names having a free occurrence inP. A name can be both free and bound in a process, for example in Q1 :=

x!hyi.z?(x).0 the first occurrence of x is free and the second is bound. The second occurrence is a placeholder and should be thought of as different name than the first. Changing the name of the second occurrence does not change the behaviour of the process, for example Q₂ := x!hyi.z?(u).0is essentially the same asQ₁.

Recall processP₁ =x?(y).y!hzi.0|x!hui.0from example 3.2. The component on the right-hand side sends the name u and continues behaving as 0. On the other hand, the component on the left-hand side receives the name u and continues behaving as u!hzi.0, that is, every free occurrence of y in y!hzi.0 is replaced byu. Thus,P₁ evolves to u!hzi.0|0.

When processes receive names, we must substitute names for names. More precisely, we want to substitute the free occurrences of y in P, when x?(y).P receives a name via x. However, we need to be careful with name conflicts;

substitutingz byy inx?(y).y!hzi.0 results to x?(y).y!hyi.0, which is not what we want. Before the substitution we should change the bound occurrences of yto, sayu, and we will end up tox?(u).u!hyi.0.

Next we give formal definitions for substitution andα-convertibility.

(11)

Definition 3.4. A substitution is a function σ : N → N, such that σ(x) 6=

x for x ∈ N ⊂ N, where N is finite, and σ(x) = x otherwise. We write {y₁, . . . , y_n/x₁, . . . , x_n}for such substitution, thatN ={x₁, . . . , x_n}andσ(x_i) = y_i fori= 1, . . . , n.

If P is a process and there is no occurence of y in P, then the process obtained by substituting every free occurrence ofxbyy is denoted byP{y/x}.

Definition 3.5. Let P be a process. Replacing a subterm x?(y).Q or subterm (υy)QofP byx?(u).Q{u/y}or(υu)Q{u/y}, respectively, is called a change of bound names. We say that processes P and P⁰ are α-convertible, if P (or P⁰) can be obtained fromP⁰ (orP) by a finite number of changes of bound names.

As we have seen previously, substituting free occurrences of names can lead to name conflicts with bound names. By Definition 3.5 we can always rename bound occurrences. Therefore, we can give the following definition for application of substitution.

Definition 3.6. LetP be a process. The process obtained by applying a substi- tutionσ to P, denoted by P σ, is obtained by replacing every free occurrence of xinP byσ(x)withα-conversion whenever needed, that is,σ(x)must be free in P σ.

For example

• (x!hyi.z?(y).y!hzi.0){z/y}=x!hzi.z?(y).y!hzi.0

• (x!hyi.z?(y).y!hzi.0){y/z}=x!hyi.y?(u).u!hyi.0

• (x!hyi.z?(y).y!hzi.0){u, v/y, z}=x!hui.v?(y).y!hvi.0.

Note. Substitution has the highest precedence. For example x!hyi.P σ =x!hyi.(P σ).

3.2 Operational Semantics

Operational semantics, that is, the behaviour of processes in π-calculus, is defined by thereductionrelation, denoted by−→. A processP reducesto process Q,P −→Q, ifP has two parallel subprocesses, sayP⁰, P⁰⁰, andP can evolve to Qas a result ofP⁰andP⁰⁰communicating. Reduction is formally defined in Defi- nition 3.13 and reduction rules are given in Table 3.2. Before defining reduction, we need to have tools to manipulate term-structure.

(12)

We have α-convertibility to identify processes that differ only in the choice of bound names. Similarly our intuition identifies for example processes P |Q andQ|P. Structural congruence is the relation to identify processes that have intuitively the same behaviour, that is, represent the same process.

To define structural congruence, denoted by ≡, we first definecontext and congruence.

Definition 3.7. A term obtained by replacing an occurence of0in a process by thehole[·]is called a context. IfC is a context andP is a process, the result of replacing the hole inC byP is denoted byC[P].

For example

C :=x?(y).[·]

is a context and

P :=u!hvi.0, Q:=y!hxi.0,

C[P] =x?(y).u!hvi.0and C[Q] =x?(y).y!hxi.0.

Note thaty∈fn(Q), buty /∈fn(C[Q]).

Definition 3.8. LetR be an equivalence relation on processes. The relationR is acongruence, if for every contextCand processesP, Q

ifP

R

Q, thenC[P]

R

C[Q].

Definition 3.9. Structural congruence (for π-calculus), denoted by ≡, is the smallest congruence on processes such that

1. if processesP andQareα-convertible, thenP ≡Q, 2. ≡satisfies the axioms in Table 3.1.

Other intuitive results can be inferred from the axioms. For example(υx)P ≡

(13)

SC-ASSOC P |(Q|R)≡(P |Q)|R

SC-COMM P |Q≡Q|P

SC-INACT P |0≡P

SC-RES (υx) (υy)P ≡(υy) (υx)P

SC-RES-INACT (υx)0≡0

SC-RES-COMP (υx) (P |Q)≡P |(υx)Q, ifx /∈fn(P)

SC-REP ∗P ≡P | ∗P

Table 3.1: Axioms for structural congruence

P for all such processesP thatx /∈fn(P):

(υx)P ≡(υx) (P |0) (SC-INACT)

≡P |(υx)0 (SC-RES-COMP)

≡P |0 (SC-RES-INACT)

≡P. (SC-INACT)

Next we give a few examples to demonstrate how term-structure can be ma- nipulated using structural congruence.

Example 3.10. SupposeP :=x?(y).(R₁|R₂)andQ:=x?(y).(R₂|R₁). We want to prove that P ≡ Q. In the previous example we used the axioms. However, none of them can be used in this case. Therefore, we need to find a suitable context and use the definition of congruence (Definition 3.8).

Consider context C := x?(y).[·]. By (SC-COMM) R₁|R₂ ≡ R₂|R₁. Then, P =C(R₁|R₂)≡C(R₂|R₁) =Q.

By Definition 3.8 C(P) ≡C(Q), wheneverP ≡Q. The other direction is not true in general.

Example 3.11. Consider processes P := x!hvi.0 and Q := y!hvi.0. Clearly P

(14)

andQare not structurally congruent. Now supposeC:= (υx) (υy) [·]. Then, C(P)≡(υx) (υz) (x!hvi.0) (α-convertibility)

≡(υy) (υz) (y!hvi.0) (α-convertibility)

≡(υy) (υx) (y!hvi.0) (α-convertibility)

≡(υx) (υy) (y!hvi.0) (SC-RES)

=C(Q).

Example 3.12. SupposeR := (υx)P |(υx)Q,z /∈fn(P), z does not occur inQ andQ⁰ :=Q{z/x}. Then

R≡(υx)P |(υz)Q{z/x} (α-convertibility)

≡(υz) ((υx)P |Q⁰) (SC-RES-COMP)

≡(υz) (Q⁰|(υx)P) (SC-COMM)

≡(υz) (υx) (Q⁰|P) (SC-RES-COMP)

≡(υx) (υz) (Q⁰|P) (SC-RES)

≡(υx) (υz) (P |Q⁰). (SC-COMM)

Note that in the previous example the occurences of xin(υx)P and(υx)Q are different binding occurrences and represent different names. Thus, we have to use α-convertibility and have certain assumptions about z before using the axioms for structural congruence.

It is always possible to use α-convertibility so that all binding occurrences are distinct from the free names and other binding occurrences. Therefore, from now on in any mathematical context we use Barendregt’s variable convention, that is,

1. no name can be both free and bound,

2. no name can be binding with two different scopes.

Next we define reduction. The rules of the form P rem₁ . . . P rem_n

Conc

are called inference rules, meaning that the conclusion, Conc, can be inferred from thepremises,P rem₁, . . . , P rem_n.

(15)

R-COM

x!hyi.P |x?(z).Q−→P |Q{y/z}

R-PAR P −→Q

P |R−→Q|R

R-RES P −→Q

(υx)P −→(υx)Q

R-STRUCT P⁰ ≡P P −→Q Q≡Q⁰

P⁰ −→Q⁰ Table 3.2: Rules for reduction

Definition 3.13. Reduction (forπ-calculus), denoted by−→, is a relation defined by the rules in Table 3.2. The reflexive and transitive closure of −→is denoted by−→^∗.

We call a proof of a reduction a reduction derivation, which is viewed as a tree, whose leaves are usages of rule R-COM and root is the reduction that is derived.

Rule R-COM is the base rule for reduction. A process consisting of two components can evolve, when the components are prefixed by the same name with opposite behaviours, that is, one can send and the other can receive. Rules R- PAR and R-RES inductively specify that communication can occur inside composition and scope restriction. For example(υx) (x!hyi.P |x?(z).Q) reduces to (υx) (P |Q{y/z}) by R-RES and R-COM. The last rule, R-STRUCT, specifies that processes can be restructured before and after reduction and reduction is still preserved. By R-STRUCT (and R-COM) we can for example prove a reduction as simple asx?(z).Q|x!hyi.P −→Q{y/z} |P.

Recall processes Server := ∗x?(y).y!hvi.0 and Client := x!hzi.z?(w).0 in

(16)

Example 3.2. Now Server|Client

≡(x?(y).y!hvi.0|Server)|Client (SC-REP)

≡(Client|x?(y).y!hvi.0)|Server (SC-COMM and SC-ASSOC)

= (x!hzi.z?(w).0|x?(y).y!hvi.0)|Server

−→(z?(w).0|(y!hvi.0){z/y})|Server (R-COM and R-PAR)

= (z?(w).0|z!hvi.0)|Server (Substitution)

≡(z!hvi.0|z?(w).0)|Server (SC-COMM)

−→(0|0{v/w})|Server (R-COM)

= (0|0)|Server (Substitution)

≡Server. (SC-INACT twice)

Therefore, by R-STRUCT

Server|Client−→(z?(w).0|(y!hvi.0){z/y})|Server−→Server andServer|Client−→^∗ Server.

Consider process (Server|Client)|z?(u).P. Like above,Server andClient can communicate viax. The process evolves to

((z?(w).0|z!hvi.0)|Server)|z?(u).P,

which in turn has two ways to evolve: viazusing eitherz?(w).0orz?(u).P (after a few usages of SC-COMM and SC-ASSOC). Thus, the continuation ofClient, that is, z?(w).0, waiting on channel z might never get any answer. We can fix this issue by changingClientto create a private channel before communicating withServer:

Client_{P RIV} := (υz)x!hzi.z?(w).0.

In Server|Client_{P RIV} we can move (υz) to the beginning by SC-RES-COMP.

Then, using R-RES the communication proceeds like above. However, this time with a private channelz.

To infer a reduction, say P −→ Q, we usually have to manipulate the term- structure of P to bring the correct terms next to each other in correct order so that R-RES, R-PAR and R-COM can be used. Then, using R-STRUCT we can infer P −→ Q. Because composition is associative and commutative, we can

(17)

freely change the order of the components. Then, it is easy to show that R1|x!hyi.P |R2|x?(z).Q|R3 −→R1|P |R2|Q{y/z} |R3 and R₁|x?(z).Q|R₂|x!hyi.P |R₃ −→R₁|Q{y/z} |R₂|P |R₃ for all processesP, Q, R₁, R₂, R₃.

How a process evolves can drastically change due to the order of reductions.

Example 3.14. Consider process

P :=x?(v).y?(w).x?(u).0|x!hai.0|x!hbi.y!hci.0.

If the first two components in the composition interact, the process reduces to y?(w).x?(u).0|0|x!hbi.y!hci.0.

The subprocess in the middle terminates and two other subprocesses can not interact. Therefore, the process is deadlocked. If, on the other hand, the first and the third component had interacted in P, the process would have reduced to

y?(w).x?(u).0|x!hai.0|y!hci.0.

Then, the first and the third component would have been able to interact again.

The previous process would have first reduced to x?(u).0|x!hai.0|0.

and finally to0|0|0≡0.

Next two examples show reduction derivations.

Example 3.15. LetP := (υx) (x!hyi.0|x?(z).0). ThenP −→0.

Proof.

x!hyi.0|x?(z).0−→0|0{y/z}R-COM

(υx) (x!hyi.0|x?(z).0)−→(υx) (0|0{y/z})R-RES where

(υx) (0|0{y/z}) = (υx) (0|0)≡0.

Therefore, by R-STRUCTP −→0.

(18)

Example 3.16. Let

P := (υx) (R|(x!hyi.0|x?(z).z!hvi.0))and Q:= (υx) (R|y!hvi.0).

ThenP −→Q.

Proof. We show the derivation in two parts. Firstly x!hyi.0|x?(z).z!hvi.0−→y!hvi.0

(x!hyi.0|x?(z).z!hvi.0)|R−→y!hvi.0|RR-PAR

R|(x!hyi.0|x?(z).z!hvi.0)−→R|y!hvi.0 R-STRUCT

(υx) (R|(x!hyi.0|x?(z).z!hvi.0))−→(υx) (R|y!hvi.0) R-RES where

Further,

x!hyi.0|x?(z).z!hvi.0−→0|(z!hvi.0){y/z} ≡y!hvi.0R-COM

x!hyi.0|x?(z).z!hvi.0 −→y!hvi.0 R-STRUCT

This finishes our introduction ofπ-calculus. We presented only basics of the calculus and the reader can refer to aforementioned books [10], [11] for more information.

3.3 Session primitives

The main session primitive is session restriction (or session creation). Interac- tion between two processes in a session needs to be private. Different syntax has been used for it in the literature. For example accept/request in [3], co- variables in [16] and [9] or polarities in [5]. We use co-variables and follow the syntax in [9] excluding data values. Though we exclude data values from the syntax for simplicity, we sometimes use them in examples for illustration purposes. Examples of languages with Boolean values can be found for example

(19)

in [16] and [17].

In session restriction two names are created and binded together as co- variables. We also introduce external and internal choice, which denote the offering of options and the selection of an option, respectively. These will be explained below. We use the same name for the language, π-calculus with sessions, as in [9].

We assume a countably-infinite set L oflabels distinct fromN (names), denoted byl, l1, l2, . . .. In examples we sometimes use meaningful words, such as set,read, etc.

Definition 3.17. (π-calculus with sessions)The processes of session-calculus are given by syntax

P ::= P |P⁰ (composition)

(υx)P (standard channel restriction)

(υxy)P (session channel restriction)

∗P (replication)

0 (inaction)

x?(y).P (input)

x!hyi.P (output)

x /l.P (selection)

x .{l_i :P_i}_i∈I (branching)

In(υxy)P x6=y,xyis an unordered pair andx, y are both binding with scopeP. We callx, y co-variables. Becausexyis an unordered pair,(υxy)P = (υyx)P.

Branching offers a set of options calledbrancheswith pairwise distinct labels.

P in x?(y).P, x!hyi.P, x /l.P and P_i in x .{l_i : P_i}i∈I are called continuation processes.

We say that processesx?(y).P,x!hyi.P,x/l.P andx.{l_i :P_i}i∈I areprefixed at namex.

Notation. We write

(υex)P for(υx1) · · ·(υxn)P and

(υxy)f P for(υx₁y₁) · · ·(υx_ny_n)P,

wheren ∈ {0,1,2, . . .}. We say thatv is inxe(orv is infxyorvuis inxy), denotedf

(20)

byv ∈ xe(or v ∈ xyf orvu ∈ fxy), ifv = x_i (orv ∈ {x_i, y_i} orvu =x_iy_i) for some i∈ {1,2, . . .}.

The syntax forπ-calculus with sessions is almost the same as forπ-calculus.

The difference is that three new primitives are added, namely session channel restriction, selection and branching.

Note. Session restriction has the same precedence as standard restriction.

Therefore, composition has the weakest precedence, substitution the highest and others the same.

We extendα-convertibility to session restriction and follow Barendregt’s variable convention.

Co-variables represent opposite ends of a session channel and interaction between them is possible. External choicex .{l_i :P_i}i∈I, which we call branching, offers options and after selection behaves according to the selection, that is, continues behaving asP_j, when labell_j is chosen. Internal choicex /l.P, which we callselection, chooses one option labeled land continues behaving asP.

We illustrate these new primitives with an example.

Example 3.18. Consider process (υxy) (x?(z).P |y!hvi.Q). Because x and y are co-variables, interaction between them is possible. The process evolves to (υxy) (P{v/z} |Q).

Communication via standard channels is possible under a session restriction.

Process(υxy) (a?(z).P |a!hvi.Q)evolves to(υxy) (P{v/z} |Q).

Recall the session type from introduction describing a server that gives op- tionslengthandconcatto get the length of a string or to concatenate two strings, respectively. Let us assume that integer and string values are added to the above syntax, |s| denotes the length of a string s and s1 +s2 denotes the con- catenation of stringss₁ ands₂. Then,

StringServer:=∗T hread,

T hread:=a?(z).z .{length:z?(str).z!h|str|i.0,

concat:z?(str₁).z?(str₂).z!hstr₁ +str₂i.0}

implements the specification. StringServer is waiting on a standard channel a

(21)

SC-RES-S-RES (υxy) (υv)P ≡(υv) (υxy)P SC-RES-S (υxy) (υvw)P ≡(υvw) (υxy)P

SC-RES-S-INACT (υxy)0≡0

SC-RES-S-COMP (υxy) (P |Q)≡P |(υxy)Q, ifx, y /∈fn(P) Table 3.3: New axioms for structural congruence forπ-calculus with sessions

for an endpoint of a session channel (withz as a placeholder). Further, StringClient:= (υxy)ClientBody

ClientBody:=a!hyi.x /concat.x!htext1i.x!htext2i.x?(text).0

implements a client selecting concat. StringClient creates two endpoints of a session channel and sends the other, y, via a to StringServer. After that, the server and the client can communicate privately viaxandy.

For operational semantics we define structural congruence and reduction as we did for π-calculus. The axioms for structural congruence are the same as before (Table 3.1) except that axioms for session restriction are added. For reduction there are three new rules, R-COM-SESS, R-SELECT and R-RES- SESS. Definitions for context and congruence are adapted to the new syntax.

Definition 3.19. Structural congruence (for π-calculus with sessions), denoted by≡, is the smallest congruence on processes such that

1. if processesP andQareα-convertible, thenP ≡Q, 2. ≡satisfies the axioms in Tables 3.1 and 3.3.

Definition 3.20. Reduction (forπ-calculus with sessions), denoted by−→, is a relation defined by the rules in Tables 3.2 and 3.4. The reflexive and transitive closure of−→is denoted by−→^∗.

Note that in rules R-COM-SESS and R-SELECT there are only two parallel processes under the restriction. Therefore, interaction can not occur viaxandy in process

(υxy) (x!hvi.P |y?(z).Q|x?(w).R).

(22)

R-COM-SESS

(υxy) (x!hvi.P |y?(z).Q)−→(υxy) (P |Q{v/z})

R-SELECT j ∈I

(υxy) (x .{l_i :P_i}i∈I |y /l_j.Q)−→(υxy) (P_j|Q)

R-RES-SESS P −→Q

(υxy)P −→(υxy)Q

Table 3.4: New rules for reduction forπ-calculus with sessions

However, in process

(υxy) (x!hvi.P |y?(z).Q|a?(w).0)

interaction can occur via x andy, because by SC-RES-S-COMP we can move a?(w).0out of the restriction. Then, by R-PAR and R-COM-RESS the interaction is possible. To summarise, any process of the form

(υxy) (x!hvi.P |y?(z).Q|R), wherex, y /∈fn(R)can reduce to

(υxy) (P |Q{v/z} |R)

by SC-RES-S-COMP and R-STRUCT (with R-PAR and R-COM-RESS).

Note. As noted above, composition is associative and commutative. Thus, we can freely change the order of the components. We sometimes want to empha- sise the usages of structural congruence, substitutions and rules R-STRUCT and R-PAR, but otherwise we skip them to make the examples shorter and easier to read.

Though interaction can not occur viaxandyin process (υxy) (x!hvi.P |y?(z).Q|x?(w).R),

it can occur viaxby R-COM and R-RES-SESS. This conflicts with the interpre- tation that co-variable represents only one end of a session channel. However, this process is not correctly typed in the type system (Section 4).

(23)

Example 3.21. Recall

StringServer=∗T hread

T hread=a?(z).z .{length:z?(str).z!h|str|i.0,

concat:z?(str₁).z?(str₂).z!hstr₁+str₂i.0}

and

StringClient = (υxy)ClientBody

ClientBody =a!hyi.x /concat.x!htext₁i.x!htext₂i.x?(text).0 from Example 3.18. Then,

StringClient|StringServer

≡(υxy)ClientBody|T hread|StringServer (SC-REP)

≡(υxy) (ClientBody|T hread)|StringServer (SC-RES-S-COMP)

−→(υxy) (x /concat. . . . |y .{. . .})

|StringServer (R-COM, R-RES)

−→(υxy) (x!htext₁i.x!htext₂i.x?(text).0

|y?(str₁).y?(str₂).y!hstr₁+str₂i.0)

|StringServer (R-SELECT)

−→(υxy) (x!htext₂i.x?(text).0

|y?(str2).y!htext1+str2i.0)

|StringServer (R-COMM-SESS)

−→(υxy) (x?(text).0|y!htext₁+text₂i.0)

|StringServer (R-COMM-SESS)

−→(υxy) (0|0)|StringServer (R-COMM-SESS)

≡StringServer.

(24)

4 Types

In Section 3.3, we saw that session channels behave slightly differently than standard channels. These differences become apparent, when typing rules are given later in Section 4.2. The main difference is that standard channels always have the same type, but the type of session channels changes during a derivation. Session types describe interaction, which changes whenever one part of the conversation is completed. Further, session types have more restrictions.

For example standard channels might occur in multiple threads, that is, in multiple parallel (sub)processes, while session channels occur in exactly one. For example process

(υxy) (x!hvi.P |y?(z).Q|x?(w).R),

is not valid, because x occurs in both x!hvi.P and x?(w).R. In this section we extend our language with types. It is structured the same way as Section 3: we first present syntax for types and continue with typing rules.

4.1 Syntax

We use the syntax in [9] except we do not have data types. However, we sometimes use them in examples for illustration purposes like before.

Definition 4.1. Thetypesof the session-calculus are given by syntax

T ::= #T (channel type)

S (session type)

S ::= end (termination)

?T.S (input)

!T.S (output)

&hl_i :S_iii∈I (branch)

⊕ hl_i :S_iii∈I (select)

We use T, T₁, T₂, . . . and U, U₁, U₂, . . . to range over types and S, S₁, S₂, . . . to range over session types. Labelsli,i∈ I, are pairwise distinct and the order of labelled items does not matter. S in?T.S,!T.S andS_iin&hl_i :S_iii∈I,⊕hl_i :S_iii∈I

are calledcontinuation types.

Typeenddescribes a terminated session. Input type ?T.S describes a (ses-

(25)

sion) channel that receives a name of typeT and continues interacting according to typeS. Similarly, output type !T.S describes a channel that sends a name of type T and continues interacting according to type S. Branch type and select type describe channels offering and selecting options, respectively, and contin- uing interacting according to type S_i (depending on the choice of a label). A standard channel of type#T sends or receives a name of typeT and continues interacting according to the same type#T.

When interaction partners follow a protocol, they need to have dual behaviour: whenever one sends, the other receives and whenever one selects, the other offers options. Duality guarantees that the interaction proceeds in a correct manner.

Definition 4.2. Duality, denoted by ·, is a relation defined recursively by the following equations:

end=end

?T.S = !T.S

!T.S = ?T.S

&hl_i :S_iii∈I =⊕hl_i :S_iii∈I

⊕hli :Siii∈I = &hli :Siii∈I

Note thatS =Sfor all session typesS. Next we give a few informal examples about typed processes.

Example 4.3. Recall

StringServer=∗T hread

T hread=a?(z).z .{length:z?(str).z!h|str|i.0

concat:z?(str1).z?(str2).z!hstr₁+str2i.0}

and

StringClient = (υxy)ClientBody

ClientBody =a!hyi.x /concat.x!htext₁i.x!htext₂i.x?(text).0

(26)

from Example 3.18 and types

Sserver1 := ?string.!int.end,

S_server2 := ?string.?string.!string.end,

S_server := &hlength:S_server1,concat:S_server2i, Sclient1 := !string.?int.end,

S_client2 := !string.!string.?string.end,

S_client:= ⊕hlength :S_client1,concat:S_client2i

from introduction. Suppose the type of a channel a is #Sserver, that is, a is capable of sending or receiving a name of type S_server. Then, the type of y in StringClient (and the type of z in StringServer) must be S_server. Further, the type of x must be S_server = S_client, because x and y are co-variables. The interaction continues as described by (dual) types S_server2 and S_client2, that is, the client sends two strings and receives one and vice versa for the server.

Therefore,StringClientandStringServerare correctly typed, when the type of ais#S_server.

4.2 Typing rules

We now have syntax for types. However, it does not tell, whether a process conforms with a type. With typing rules we can find out, whether a typing is correct or incorrect. In this section we present typing rules formally, explain every rule and give examples, how a typing for a process can be validated.

Before presenting the typing rules for the type system, we definetype environment and introduce related terminology.Γ`P is atype judgement asserting that process P uses names according to the assignments in Γ. We write x : T for an assignment of typeT to namex. Typing rules in this section are adapted from [5] except we do not introduce recursive types or subtyping.

Definition 4.4. Atype environment (or anenvironment) is a partial function from names to types, denoted by Γ. We say that type environmentΓassigns typeT to namex, ifΓ(x) = T. We write

x₁ :T₁, . . . , x_n:T_n

for such environment that assignsTi toxi,i∈ {1, . . . , n}and is undefined other-

(27)

wise. We say thatx(orx :T) is inΓorΓcontainsx(orx :T), ifΓ(x)is defined (and Γ(x) = T). Occurrences of names in an environment Γ are not bound.

Therefore, they are distinct from all binding occurrences of names.

If Γ₁ and Γ₂ have disjoint domains, we write Γ₁,Γ₂ for such an environment that assigns to each namex∈dom(Γ₁)∪dom(Γ₂)typeΓ₁(x), ifΓ₁(x)is defined, or typeΓ₂(x), ifΓ₂(x)is defined, and is undefined otherwise.

LetP be a process. We say that environmentΓis

1. completed, if only session type in the range ofΓisend, 2. unlimited, if there are no session types in the range ofΓ,

3. unlimited forP, ifΓis completed and for everyxinΓthe following holds:

ifΓ(x) =end, thenx /∈fn(P).

In a completed environment every session channel has completed its interactions, that is, every session channel has communicated in a correct manner. In an unlimited environment there are no session types. However, during the evolu- tion of a process session channels can be created and, therefore, session types can be added to an environment during a typing derivation. An environment that is unlimited for a specific process can contain completed session types, but the process cannot contain any session channels typed by those session types.

Some of the typing rules use addition operation on environments. This guarantees that session channels are not used by multiple parallel processes. Ses- sion channels can only be added to an environment, if they do not already exist there, while standard channels can be added as many times as needed, whenever the type of the channel does not change. Thus, addition is a partial operation. It is implicitly assumed in the typing rules that the addition of environments is defined.

Definition 4.5. Additionon environments, denoted by +, is a partial binary operation defined inductively by the following rules:

x /∈dom(Γ)

Γ +x:T = Γ, x:T (Γ, x: #T) +x: #T = Γ, x: #T

(28)

T-NIL Γcompleted

Γ`0 T-PAR Γ₁ `P Γ₂ `Q

Γ₁+ Γ₂ `P |Q T-REP Γ`P Γunlimited forP

Γ` ∗P T-RES Γ, x: #T `P

Γ`(υx)P T-RES-S Γ, x:S, y :S`P Γ`(υxy)P T-IN Γ, x: #T, y:T `P

Γ, x: #T `x?(y).P T-IN-S Γ, x:S, y :T `P Γ, x: ?T.S `x?(y).P

T-OUT Γ, x: #T `P

(Γ, x: #T) +y:T `x!hyi.P

T-OUT-S Γ, x:S `P

(Γ, x: !T.S) +y:T `x!hyi.P

T-SELECT j ∈I Γ, x:S_j `P

Γ, x:⊕hli :Siii∈I `x /lj.P T-BRANCH ∀i∈I Γ, x:S_i `P_i

Γ, x: &hl_i :S_ii_i∈I `x .{l_i :P_i}_i∈I Table 4.1: Typing rules for session-calculus

SupposeΓ :=x:S₁, z : #T₁. Then,

Γ, z : #T₁ andΓ +z : #T₂ are not defined, Γ +z: #T₁ = Γ,

Γ, x:S₁ andΓ +x:S₁ andΓ +x:S₂ are not defined, Γ +y:S₂ = Γ, y :S₂,

Γ +z: #T₁, v : #T₂, y :S₂ = Γ, v : #T₂, y :S₂, Γ +z: #T₁, v : #T₂, x:S₁ is not defined.

We now have all the machinery in place to present the typing rules. We call a proof of a type judgement atyping derivation, which is viewed as a tree, whose leaves are usages of rule T-NIL and root is the judgement that is derived. We explain every rule below and give a few example derivations.

(29)

Definition 4.6. We say that processP iswell-typed (orcorrectly typed) in Γ, if Γ`P can be inferred from the rules in Table 4.1. IfP is well-typed inΓ, we say that Γ ` P is valid and often write just Γ ` P. Otherwise we say that Γ ` P is invalid andP isill typed orincorrectly typed inΓ.

Note. IfΓ, x: T ` P, then xis either free inP or there are no occurrences of x inP. This follows from the variable convention.

For example, x: #T `(υx)P is ill formed, because the first occurrence of x is free and the second is bound.

T-SELECT and T-BRANCH are rules for typechecking selection and branching, respectively. Selection x /l_j.P, where the type ofx is ⊕hl_i : S_iii∈I, is well- typed, if the label exists and the continuation processP usesxwith continuation type S_j. Branching x .{l_i : P_i}i∈I, where the type of x is &hl_i : S_iii∈I, is well- typed, if each of the continuation processes P_i, i ∈ I, use x with continuation typeS_i.

Rules T-IN and T-IN-S are used to typecheck input for standard channels and session channels, respectively. Input x?(y).P, where the type of x is either #T or?T.S, is well-typed, if the type ofyisT and continuation processP usesxwith the same type#T for standard channels or with continuation typeSfor session channels.

Rules for output x!hyi.P, T-OUT and T-OUT-S, are similar to the rules for input. However, this time y : T is added to the environment in the conclusion.

Note that addition is not defined, if already existing session channel is added.

Therefore, T-OUT and T-OUT-S prevent sending a session channel, if it is already in the environment. This guarantees that a session channel occurring in the continuation processP is not sent to another subprocess running in parallel.

T-RES and T-RES-S are rules for standard and session channel restriction, respectively. Session channel restriction(υxy)P is well-typed only, when xand yhave dual (session) types and processP uses them with those types.

Rule T-PAR is used to typecheck compositionP |Q; It is well-typed, if the environment can be split to two such parts,Γ₁ andΓ₂, thatP is well-typed inΓ₁ and Qis well typed in Γ₂. Again, addition of environments Γ₁ andΓ₂ is not defined, if they both contain same session channel. This guarantees (together with the rules for output) that no session channel is used in two parallel subprocesses.

Replication ∗P is well-typed in Γ by T-REP, if P is well-typed in Γ and Γ is unlimited forP.

(30)

Finally, T-NIL is the base rule; Inaction 0 is well-typed in every environment containing no session types except end. T-NIL ensures session channels are not discarded before fully used. However, as pointed out in [5], the type system does not prevent deadlocks. For example, type judgement

x:?#T.end, y :!#T.end, u:?#T.end, v :!#T.end, a: #T

`x?(z).v!hai.0|u?(w).y!hai.0,

where x, y are co-variables and so are u, v, is valid, but the process is deadlocked.

Example 4.7. We show a type derivation for the previous type judgement. Only one of the parallel subprocesses is derived, because the derivations are similar.

By T-PAR we can derive the previous type judgment from the two jugdements below

x:?#T.end, v :!#T.end+a : #T `x?(z).v!hai.0 y:!#T.end, u:?#T.end+a : #T `u?(w).y!hai.0 The derivation for the first judgement is

x:end, z : #T, v:end

x:end, z : #T, v :end`0 T-NIL

x:end, z : #T, v:!#T.end+a: #T `v!hai.0T-OUT-S

x:?#T.end, v :!#T.end+a: #T `x?(z).v!hai.0 T-IN-S

Note that in T-PARa: #T can be in both sides, because#T is standard channel type. Therefore, the addition in the conclusion is defined. In addition, T-NIL could not have been used, if#T was not a standard channel type orend.

Another form of deadlock is, when both ends of a session channel occur in the same thread. For example,

v :end`(υxy)x!hvi.y?(u).0

is valid, but the process is deadlocked. The typechecking algorithm in [5] elim- inates deadlocks of this form. However, it does not eliminate deadlocks of the previous form.

(31)

Example 4.8. Type derivation for the previous judgement is x:end, y :end, u:end

x:end, y :end, u:end`0T-NIL

x:end, y :?end.end`y?(u).0 T-IN-S x:!end.end, y :?end.end, v :end`x!hvi.y?(u).0

v :end`(υxy)x!hvi.y?(u).0 T-RES-S

T-OUT-S

A process can be well-typed in one environment and ill typed in another:

Example 4.9. Consider process P := x?(u).0|x?(v).0and environments Γ₁ :=

x:?T.endandΓ₂ := x: #T. Then,P is ill typed in Γ₁. Further,P is well-typed in Γ2, ifT is a standard channel type orend.

Addition x : #T +x : #T = x : #T is defined, because x is a standard channel. Therefore, we can derive

x: #T, u:T

x: #T, u:T `0T-NIL x: #T `x?(u).0 T-IN

x: #T, v:T

x: #T, v :T `0T-NIL x: #T `x?(v).0 T-IN

x: #T +x: #T `x?(u).0|x?(v).0 T-PAR

Therefore,Γ₂ `P is valid. Again, T-NIL could not have been used, if T was not a standard channel type orend.

Typing P in Γ1 would require splitting the environment in two parts. Both parts should contain x :?T.end. However, additionx :?T.end+x :?T.endis not defined and thus T-PAR cannot be used. Therefore,P is not well-typed inΓ₁. Example 4.10. We show that

a: #S_server `StringServer

(see Example 4.3) is valid. We assume types and expressions for integers and strings are added to the syntax and omit the details. We writeS S₁,S₂,len and ccforS_server,S_server1,S_server2,lengthandconcat, respectively.

The environment a : #S contains no session types and is thus unlimited.

Therefore, rule T-REP can be used as the last rule in the derivation below. We show the derivation in three parts; from usage of T-BRANCH to T-REP and sep- arately to both branches from T-NIL until T-BRANCH.

(32)

The last part of the derivation is

a: #S, z:S₁ `P_len a: #S, z :S₂ `P_cc

a: #S, z: &hlen:S₁,cc:S₂i `z .{len:P_len,cc:P_cc}T-BRANCH a: #S `a?(z).z .{len:P_len,cc:P_cc}

a: #S ` ∗T hread T-REP

T-IN

whereP_len := z?(str).z!h|str|i.0and P_cc := z?(str₁).z?(str₂).z!hstr₁ +str₂i.0 are the continuation processes for labelslenandcc. Derivation for thelenbranch is

a : #S, z :end, str :string

a: #S, z :end, str :string`0T-NIL

a: #S, z:!int.end, str :string `z!h|str|i.0T-OUT-S

a: #S, z : ?string.!int.end`z?(str).z!h|str|i.0 T-IN-S and forccbranch

a : #S, z :end, str1 :string, str2 :string a: #S, z :end, str1 :string, str2 :string`0

a: #S, z :!string.end, str1 :string, str2 :string `z!hstr₁+str₂i.0 a: #S, z :?string.!string.end, str₁ :string`z?(str₂).z!hstr₁+str₂i.0 a: #S, z: ?string.?string.!string.end`z?(str₁).z?(str₂).z!hstr₁+str₂i.0

(33)

5 Type soundness

In this section we prove type preservation with respect to operational semantics.

Furthermore, we prove that well-typed processes use session types in a correct manner. Together these two results form type soundness. We first prove a few properties to help proving the main results.

We follow a similar process for proving type soundness as in [5] and [16].

The theorems are mostly adapted from [5]. However, due to differences in the syntax, especially in the syntax for session restriction, proofs are given. As this thesis is targeted for a new reader, proofs are very detailed. This, we believe, makes it easier to understand the theory and gives confidence for the reader to continue her adventure in the world of session types.

In [5] subtypes and recursive types are defined for the language. We have not included those, which makes the proofs slightly simpler. The biggest difference between our language and the language in [5] is in the syntax of session channels and reduction. We have used co-variables together with separate syntax for session restriction and allowed communication for session channels only inside a restriction. In [5] optional polarities for channels are used and reductions are annotated. Furthermore, communication between session channels is possible without a restriction. Our choice, in our opinion, makes the difference between standard channels and session channels clearer. In addition, it simplifies the proofs and makes them easier to follow.

Firstly we show that, if a process is correctly typed in an environment, then every free name of the process must be in the environment. We continue by showing that in certain circumstances it is possible to weaken or strengthen an environment, that is, to add assignments to the environment or remove assignments from the environment, respectively.

Lemma 5.1. IfΓ`P, thenfn(P)⊆dom(Γ).

Proof. By induction on the derivation ofΓ`P. Induction hypothesis (IH) is, that the statement holds for the premises. Rule T-NIL is the base case.

T-NIL: Clearly fn(0) = ∅ ⊆dom(Γ).

T-PAR: By IHfn(P)⊆dom(Γ₁)andfn(Q)⊆dom(Γ₂). Then,

fn(P |Q) =fn(P)∪fn(Q)⊆dom(Γ₁)∪dom(Γ₂) = dom(Γ₁+ Γ₂).

T-REP: By IHfn(P)⊆dom(Γ). Then,fn(∗P) = fn(P)⊆dom(Γ).

(34)

T-RES: By IHfn(P)⊆dom(Γ, x: #T). Then,

fn((υx)P) =fn(P)− {x} ⊆dom(Γ, x: #T)− {x}=dom(Γ).

T-RES-S: Similar to T-RES.

T-IN: Similar to T-IN-S.

T-IN-S: By IHfn(P)⊆dom(Γ, x:S, y :T). Then, fn(x?(y).P) = (fn(P)∪ {x})− {y}

⊆(dom(Γ, x:S, y :T)∪ {x})− {y}

=dom(Γ, x:S, y :T)− {y}

=dom(Γ, x:?T.S).

T-OUT: By IHfn(P)⊆dom(Γ, x: #T). Then, fn(x!hyi.P) = fn(P)∪ {x, y}

⊆dom(Γ, x: #T)∪ {x, y}

=dom(Γ, x: #T)∪ {y}

=dom((Γ, x: #T) +y:T).

T-OUT-S: Similar to T-OUT.

T-SELECT: Similar to T-BRANCH.

T-BRANCH: By IHfn(P_i)⊆dom(Γ, x:S_i), for alli∈I. Then, fn(x .{l_i :P_i}i∈I) =[

i∈I

fn(P_i)∪ {x}

⊆[

i∈I

dom(Γ, x:S_i)∪ {x}

=dom(Γ, x:Si)for anyi∈I

=dom(Γ, x: &hl_i :S_iii∈I).

Lemma 5.2 (Weakening). Let Γ ` P. If U is a standard channel type or end andΓ, z :U is defined, thenΓ, z :U `P.

(35)

Proof. By induction on the derivation of Γ ` P. We show proofs for cases T- NIL, T-OUT, T-REP and T-PAR. Other cases are similar to T-OUT. Note that by Lemma 5.1fn(P)⊆dom(Γ). Therefore,z /∈fn(P).

T-NIL: NowΓ`0andΓis completed. ClearlyΓ, z :U is completed, whenΓ is completed. Therefore, we can deriveΓ, z :U `0.

T-REP: The only derivation forΓ` ∗P is

Γ`P Γunlimited forP

Γ` ∗P T-REP

Now,Γ, z :U is unlimited for P, becausez /∈fn(P). Then, by IHΓ, z :U ` P and we can derive

Γ, z :U ` ∗P.

T-PAR: Derivation forΓ`P |Qis

Γ₁ `P Γ₂ `Q Γ₁+ Γ₂ `P |Q

whereΓ = Γ₁+ Γ₂. By IHΓ₁, z :U `P. Then, we can derive Γ₁, z :U `P Γ₂ `Q

(Γ₁, z :U) + Γ₂ `P |Q where(Γ1, z:U) + Γ2 = (Γ1+ Γ2), z:U = Γ, z:U. T-OUT: Derivation forΓ`x!hyi.P is

Γ1, x: #T `P

(Γ₁, x: #T) +y:T `x!hyi.P

where Γ = (Γ₁, x : #T) +y : T. Becausez /∈ fn(x!hyi.P), z cannot be x nory. Then, by IHΓ1, z :U, x: #T `P and we can derive

Γ1, x: #T `P

(Γ₁, z :U, x: #T) +y:T `x!hyi.P where

(Γ₁, z:U, x: #T) +y:T = ((Γ₁, x: #T) +y:T), z :U = Γ.

(36)

Corollary 5.3. LetΓ₁ `P andΓ₂ is completed.

1. IfΓ₁,Γ₂ is defined, thenΓ₁,Γ₂ `P. 2. IfΓ₁+ Γ₂ is defined, thenΓ₁+ Γ₂ `P.

Lemma 5.4(Strengthening). LetΓ, z :T `P andz /∈fn(P).

(1) IfT is a session type, then T =end.

(2) Γ`P.

Proof. By induction on the derivation ofΓ, z :T `P. We show proofs for cases T-NIL and T-PAR below. For other cases we can simply replace Γ with Γ, z : T in the typing rules, because z /∈ fn(P). Then, by induction hypothesis the judgements in the premises are valid for the environment without z : T and we can derive Γ ` P (2). Furthermore, by induction hypothesisT has to be a standard channel type orendin the premises and, thus, in the conclusion (1).

T-NIL: Because Γ, z : T ` 0, environment Γ, z : T has to be completed.

Then, T is either a standard channel type or end (1). Further, Γ is also completed and, thus,Γ`0(2).

T-PAR: Now

Γ, z :T `P |Q, Γ₁ `P and Γ₂ `Q,

whereΓ₁+ Γ₂ = Γ, z :T andz /∈fn(P |Q). Then, if T is standard channel type, Γ₁(z) is defined, Γ₂(z) is defined or both of them are defined. If T is a session type, either Γ₁(z) or Γ₂(z) is defined. Let us assumeΓ₁(z) is defined andΓ₂(z)is not (other cases are similar). We can writeΓ₁ = Γ⁰₁, z : T. Becausez /∈fn(P |Q), z /∈fn(P)either. Thus, by IH for (2)Γ⁰₁ `P and by T-PAR

Γ⁰₁+ Γ₂ `P |Q.

Furthermore, Γ⁰₁ + Γ2 = Γ and, therefore, Γ ` P |Q(2). If T is a session type, then by IH (inΓ⁰₁, z :T `P) for (1)T must beend.

(37)

Ideally an environment should contain assignments for free names of a process only. Strengthening allows us to remove assignments from an environment one by one to get rid of assignments, which are not needed. The next result follows.

Corollary 5.5. If Γ ` P and Γis unlimited for P, then there exists an unlimited environmentΓ⁰ such thatΓ⁰ `P.

Before proving the main theorems, we now prove results for substitution and structural congruence. The result for substitution is needed, when proving preservation under reduction rules R-COM and R-COM-SESS. Preservation for structural congruence is needed to prove preservation under reduction rule R-STRUCT and to prove type safety.

Lemma 5.6(Substitution). IfΓ, v :T ` P andΓ +z :T is defined, thenΓ +z : T `P{z/v}.

Proof. By induction on the derivation ofΓ, v :T `P.

T-NIL: Clearly Γ +z : T is completed, because Γ, v : T is completed. In addition,0{z/v}=0. Then, by T-NILΓ +z :T `0{z/v}.

T-PAR: Now

Γ, v :T `P |Q, Γ₁ `P and Γ₂ `Q,

where Γ₁ + Γ₂ = Γ, v : T. Simliarly to the proof of Lemma 5.4 let us assumeΓ₁(v)is defined andΓ₂(v)is not (other cases are similar) and write Γ₁ = Γ⁰₁, v :T. By Lemma 5.1fn(Q)⊆ dom(Γ₂). Becausev is not inΓ₂,v is not in fn(Q) and, then, Q{z/v} = Q. On the other hand, Γ⁰₁, v : T ` P and clearlyΓ⁰₁+z :T is defined. Then by IH

Γ⁰₁+z :T `P{z/v}.

By T-PAR we get

(Γ⁰₁+z :T) + Γ₂ `P{z/v} |Q{z/v},

(38)

where

P{z/v} |Q{z/v}= (P |Q){z/v}and

(Γ⁰₁+z :T) + Γ₂ = (Γ⁰₁+ Γ₂) +z :T = Γ +z :T.

T-REP: Clearly Γ +z : T is unlimited forP, when Γ, v :T is unlimited for P. Then, by IHΓ +z :T `P{z/v}and by T-REP

Γ +z :T ` ∗P{z/v}

and∗P{z/v}= (∗P){z/v}.

T-RES: Now

Γ, v :T `(υx)P and Γ, v :T, x: #U `P.

By IH

Γ, x: #U+z :T `P{z/v},

whereΓ, x: #U+z :T = (Γ +z :T), x: #U is defined, because Γ +z :T is defined. Then, by T-RES

Γ +z :T `(υx)P{z/v}

and(υx)P{z/v}= ((υx)P){z/v}.

T-RES-S: Similar to T-RES.

T-IN: Similar to T-IN-S.

T-IN-S: NowΓ, v :T `x?(y).P. There are two possibilities forv: eitherv =x orv 6=x.

(v =x) We have

Γ₁, v :?U.S `v?(y).P and Γ₁, v :S, y :U `P.

By IH

Γ₁, y :U +z :S `P{z/v},

(39)

where

Γ₁, y :U +z :S = Γ₁, z :S, y :U

is defined, becauseΓ₁+z :?U.Sis defined. Then, by T-IN-S Γ₁, z:?U.S`z?(y).P{z/v},

where

Γ1, z :?U.S = Γ1 +z :?U.S and z?(y).P{z/v}= (v?(y).P){z/v}.

(v 6=x) Now

Γ₂, x:?U.S, v :T `x?(y).P and Γ₂, x:S, y :U, v:T `P.

By IH

Γ₂, x:S, y :U+z :T `P{z/v}, where

Γ₂, x:S, y :U +z :T = (Γ₂+z:T), x:S, y:U

is defined, becauseΓ₂, x:?U.S+z :T is defined. Then, by T-IN-S (Γ₂+z:T), x:?U.S`x?(y).P{z/v}

and(Γ2+z :T), x:?U.S = Γ2, x:?U.S+z :T. T-OUT: Similar to T-OUT-S.

T-OUT-S: Now Γ, v : T ` x!hyi.P. There are three possibilities for v: v = x, v =yorv 6=x, y.

(v =x) We have

(Γ₁, v :!U.S) +y:U `v!hyi.P and Γ₁, v:S `P.

By IH

Γ₁+z :S`P{z/v},

(40)

where

Γ₁+z :S = Γ₁, z :S

is defined, because(Γ₁+y:U) +z :!U.Sis defined. Then, by T-OUT-S (Γ₁, z :!U.S) +y:U `z!hyi.P{z/v},

where

(Γ1, z :!U.S) +y:U = (Γ1+y:U) +z :!U.S and z!hyi.P{z/v}= (v!hyi.P){z/v}.

(v =y) In this case

(Γ₂, x:!U.S) +v :U `x!hvi.P and Γ₂, x:S `P.

Then, eitherv is indom(Γ2)orv is not indom(Γ2).

(v ∈dom(Γ₂)) Let us writeΓ₂ = Γ⁰₂, v :U. By IH

(Γ⁰₂, x:S) +z :U `P{z/v}, where

(Γ⁰₂, x:S) +z :U = (Γ⁰₂+z :U), x:S

is defined, because (Γ⁰₂, x :!U.S) +z : U is defined. Then, by T-OUT-S

((Γ⁰₂+z :U), x:S) +y:U `x!hyi.P{z/v}

and((Γ⁰₂+z:U), x:S) +y:U = ((Γ⁰₂, x:!U.S) +y:U) +z :U. (v /∈dom(Γ₂)) Because v is not in dom(Γ₂), v /∈ fn(P) by Lemma 5.1.

Then,P{z/v}=P. By T-OUT-S

(Γ₂, x:!U.S) +z :U `x!hzi.P andx!hzi.P = (x!hvi.P){z/v}.

(41)

(v 6=x, y) Now

(Γ3, v :T, x:!U.S) +y:U `x!hyi.P and Γ₃, v :T, x:S `P.

By IH

(Γ₃, x:S) +z :T `P{z/v}, where

(Γ₃, x:S) +z :T = (Γ₃+z :T), x:S

is defined, because ((Γ₃, x:!U.S) +y:U) +z :T is defined. Then, by T-OUT-S

((Γ₃+z :T), x:!U.S) +y:U `x!hyi.P{z/v}

and((Γ₃+z :T), x:!U.S) +y:U = ((Γ₃, x:!U.S) +y :U) +z :T. T-SELECT: NowΓ, v : T ` x /l_j.P. Then, there are two possibilities for v:

eitherv =xorv 6=x.

(v =x) In this case

Γ1, v :⊕hli :Siii∈I `v /lj.P and Γ₁, v :S_j `P,

wherej ∈I. By IH

Γ₁+z :S_j `P{z/v}, where

Γ₁+z :S_j = Γ₁, z :S_j

is defined, because Γ₁ +z : ⊕hl_i : S_iii∈I is defined. Then, by T- SELECT

Γ1, z :⊕hli :Siii∈I `z /lj.P{z/v}, where

Γ1, z :⊕hli :Siii∈I = Γ1 +z :⊕hli :Siii∈I and z /l_j.P{z/v}= (v /l_j.P){z/v}.

A Gentle Introduction to Session Types

Pekka Peltola