A Language for the Declarative Composition of
Concurrent Protocols

arXiv:1602.03729v2 [] 24 Oct 2016

Luı́s Cruz-Filipe and Fabrizio Montesi
University of Southern Denmark

{lcf,fmontesi}@imada.sdu.dk

Abstract. A recent study of bugs in real-world concurrent and distributed systems found that, while implementations of individual protocols tend to be robust, the composition of multiple protocols and its
interplay with internal computation is the culprit for most errors.
Multiparty Session Types and Choreographic Programming are methodologies for developing correct-by-construction concurrent and distributed
software, based on global descriptions of communication flows. However,
protocol composition is either limited or left unchecked. Inspired by these
two methodologies, in this work we present a new language model for the
safe composition of protocols, called Procedural Choreographies (PC).
Protocols in PC are procedures, parameterised on the processes that enact them. Procedures define communications declaratively using global
descriptions, and programs are written by invoking and composing these
procedures. An implementation in terms of a process model is then mechanically synthesised, guaranteeing correctness and deadlock-freedom.
We study PC in the settings of synchronous and asynchronous communications, and illustrate its expressivity with some representative examples.

1

Introduction

In the last decades, advances in multi-core hardware and large-scale networks
have made concurrent and distributed systems widespread. Unfortunately, programming such systems is a notoriously error-prone activity. In [22], 105 randomlyselected concurrency bugs from real-world software projects are analysed. Of
these, 31 are caused by deadlocks. Of the 74 remaining ones, 97% are caused by
violations of the programmer’s intentions on atomicity or the ordering of actions.
The theory of Multiparty Session Types tackles these problems in communication protocols [18]. The idea is that developers express their intentions on
communications declaratively, by writing protocol specifications from a global
viewpoint using an “Alice and Bob” notation. Given such a global specification,
an EndPoint Projection (EPP) mechanically synthesises the local specifications
of the I/O actions for each participant. The local specifications are thus correct
by construction. Then, a type system can be used to check that implementations
in process models follow the generated local specifications. Multiparty session
types guarantee that the implementation of each protocol, taken in isolation, is
deadlock-free and faithful to its global specification – which, by its declarative
nature, respects the programmer’s intentions. However, errors can still occur

due to the composition of multiple protocol executions, which is left unchecked.
Different approaches for avoiding deadlocks in protocol compositions have been
proposed [8,9], but these limit how protocols can be composed – e.g., protocols can be instantiated only in a certain order, or connections among processes
should form a tree structure – and do not offer a means to easily and correctly
translate the programmer’s intentions on ordering: the language for composing
protocols is not declarative.
A more recent empirical study [21] reveals that protocol composition deserves more attention. It presents a taxonomy of 104 Distributed Concurrency
(DC) bugs. The authors’ findings include a significant insight, which we quote
(emphasis ours):
“Real-world DC bugs are hard to find because many of them linger
in complex concurrent executions of multiple protocols. [. . . ] Individual
protocols tend to be robust in general. Only 18 DC bugs occur in individual protocols without any input fault condition [. . . ]. On the other
hand, a large majority of DC bugs happen due to concurrent executions
of multiple protocols [. . . ]”
In this quote, a protocol is not intended as an abstract specification as in
multiparty session types, but rather as the concrete series of events that happen
in an implementation, including internal computation. This motivates us to address the problem of protocol composition in the framework of Choreographic
Programming [23]: a paradigm similar to Multiparty Session Types, where global
descriptions of communications are not used as types, but rather as programs.
In such programs, called choreographies, developers declaratively program communications among processes together with the internal computations that they
perform. EPP is then used to synthesise an implementation in terms of a process
model [5]. However, state of the art models for choreographic programming still
do not support many of the features used in real-world programs, such as those
in [21]. One prominent aspect, which is the focus of this paper, is that these models do not support arbitrary compositions of protocol executions, since they are
not modular. In particular, the absence of full procedural abstraction disallows
the development of reusable libraries that can be composed as “black boxes”.
Inspired by these observations, we propose a language model for the correct
programming of concurrent and distributed systems based on message passing,
called Procedural Choreographies (PC). PC is a new model for choreographic
programming, where we can define a protocol execution as a procedure, parameterised on the processes that will actually enact it. Composition of protocol
executions is then obtained by allowing for the arbitrary composition of procedure calls, a feature lacked by previous choreography models. Nevertheless,
PC inherits all the good properties of languages based on declarative global descriptions of communications – as in choreographic programming and multiparty
session types – and extends them to protocol compositions. In particular, the
process implementations synthesised from choreographies are correct by construction and deadlock-free. Thus, PC contributes to bringing the current body
2

of work on safe concurrent programming nearer to dealing with the kinds of bugs
analysed in [21].
Example 1. We discuss a parallel version of merge sort in PC. Although this is a
toy example, it cannot be written in any previous model for choreographic programming, thus allowing us to present the key features of our work for a simple
scenario. More realistic and involved examples are presented after the formal
presentation of PC. We make the standard assumption that we have concurrent
processes with local storage and computational capabilities. In this example,
each process stores a list and can use the following local functions: split1 and
split2, respectively returning the first or second half of a list; is_small, which
tests if a list has at most one element; and merge, which combines two sorted
lists into one. The following (choreographic) procedure, MS, implements merge
sort on the list stored at its parameter process p.1
MS ( p ) = if p . is_small then 0
else p start q1 , q2 ; p . split1 -> q1 ; p . split2 -> q2 ;
MS < q1 >; MS < q2 >; q1 .* -> p ; q2 .* -> p . merge

Procedure MS starts by checking whether the list at process p is small, in which
case it does not need to be sorted (0 denotes termination); otherwise, p starts
two other processes q1 and q2 (p start q1,q2), to which it respectively sends
the first and the second half of the list (p.split1 -> q1 and p.split2 -> q2).
The procedure is recursively reapplied to q1 and q2, which independently (concurrently) proceed to ordering their respective sub-lists. When this is done, MS
stores the first ordered half from q1 to p (q1.* -> p, where * retrieves the data
stored in q1) and merges it with the ordered sub-list from q2 (q2.* -> p.merge).
Our merge sort example showcases the key desiderata for PC:
General recursion. Procedure calls can be followed by arbitrary code.
Parameterised procedures. Procedures are parametric on their processes (p
in MS), and can thus be reused with different processes (as in MS<q1> and
MS<q2>).
Process spawning. The ability of starting new processes. There must be no
bound on how many processes can be started, since this is decided at runtime.
(In MS, the number of spawned processes depends on the size of the initial list.)
Implicit Parallelism. In the composition MS<q1>; MS<q2>, the two calls can
be run in parallel because they involve separate processes and are thus noninterfering. Thus, the code synthesised from this program should be parallel.
In the remainder, we explore more sophisticated programs that require additional features, e.g., mobility of process names.
1

In the remainder, we use a monospaced font for readability of our concrete examples,
and other fonts for distinguishing syntactic categories in our formal arguments as
usual.

3

1.1

Contributions

We summarise our development and contributions.
Procedural Choreographies. We introduce Procedural Choreographies (PC),
a new language model that supports all the features discussed above (§ 2). We
evaluate the expressivity of PC not only with our concurrent merge sort example,
but also with a more involved parallel downloader. This example makes use of
additional features: mobility of process names (networks with connections that
evolve at runtime) and propagation of choices among processes. It also makes
heavy use of implicit parallelism to deal with the parallelisation of multiple
streams.
Asynchrony. PC can be endowed with both a synchronous (§ 2) and an asynchronous semantics (§ 5). All our results hold for both versions, and the two
semantics enjoy a strong correspondence result (Theorem 6). This allows developers to reason about their programs in the simpler synchronous setting and then
to use the asynchronous semantics to obtain a more concurrent implementation,
without worrying about introducing unsafe behaviour.
Typing. Mobility of process names requires careful handling, especially its interplay with procedure composition: if a procedure specifies that two processes
interact, then they should be properly connected (know each other’s names). We
introduce a novel typing discipline (§ 3) that prevents such errors by tracking
the connections required by each procedure. It also checks that processes store
data of the correct type for the local functions that use it. PC enjoys decidable
type checking (Theorem 2) and type inference (Theorems 3 and 4).
Endpoint Projection. We define an EndPoint Projection (EPP) that, given a
choreography, synthesises a concurrent implementation in Procedural Processes
(PP), our target process calculus (§ 4). PP is an abstraction of systems where
concurrent processes communicate by referring to each other’s locations or identifiers, as it happens, e.g., in MPI [25] or the Internet Protocol. The synthesised
code is correct by construction: it faithfully follows the behaviour of the originating choreography (Theorem 5). Also, EPP is transparent, in the sense that it does
not introduce any auxiliary communications or computations. This means that
a choreography always faithfully represents the actual efficiency and behaviour
of the algorithm written by the programmer. All generated implementations are
deadlock-free by construction (Corollary 1).
Extensions. We further discuss two extensions that allow us to write more
general procedures, enhancing the expressive power of PC: allowing parameters
to be lists of processes and allowing procedure bodies to contain holes that can
be filled at runtime with arbitrary code (§ 6). These extensions can be elegantly
obtained by introducing minimal additions to the theory of PC, demonstrating
its robustness, but they are nevertheless very useful in practice.
4

C ::= η; C | I; C | 0

η ::= p.e -> q.f | p -> q[l] | p start qT | p : q <-> r

T ) = C, D | ∅
D ::= X(qf

I ::= if p.e then C1 else C2 | Xhp̃i | 0

Fig. 1. Procedural Choreographies, Syntax.

2

Procedural Choreographies (PC)

We begin by introducing the language model of Procedural Choreographies (PC).
We focus on the synchronous semantics in this section, as the underlying theory
is a bit simpler. The asynchronous model is discussed in § 5.
Syntax. The syntax of PC is displayed in Figure 1. A procedural choreography is
a pair hD, Ci, where C is a choreography and D is a set of procedure definitions.
Process names (p, q, r, . . .), identify processes that execute concurrently. Each
process is equipped with a memory cell that stores a single value of a fixed type.
Specifically, we consider a fixed set T of datatypes (numbers, lists, etc.); each
process p stores only values of type Tp ∈ T. Statements in a choreography can
either be communication actions (η) or compound instructions (I), both of which
can have continuations. Term 0 is the terminated choreography, which we often
omit in examples. We call all terms but 0; C program terms, or simply programs,
since these form the syntax intended for developers to use for writing programs.
Term 0; C is necessary only for the technical definition of the semantics, to
capture termination of procedure calls with continuations, and can appear only
at runtime. It is thus called a runtime term. This distinction plays a bigger role
in § 5, which introduces more runtime terms to track the state of asynchronous
communications.
Processes communicate via direct references (names) to each other.2 In a
value communication p.e -> q.f , process p sends the result of evaluating expression e to q. In e, the placeholder ∗ is replaced at runtime with the data stored at
process p. When q receives the value from p, it applies to it the (total) function
f and stores the result. The definition of f may also access the contents of q’s
memory.
In a selection term p -> q[l], p communicates to q its choice of label l, which
is a constant. This term is intended to propagate information on which internal
choice has been made by a process to another (see Remark 2 below).
In term p start qT , process p spawns the new process q, which stores data of
type T . Process name q is bound in the continuation C of p start qT ; C.
Process spawning introduces the need for mobility of process names. In realworld systems, after execution of p start qT , p is the only process that knows the
2

This makes PC easy to apply to mainstream settings based on actors, objects, or
ranks (e.g., MPI). We could give a formulation of PC based on standard channels
(from process calculi), where each pair of process names is a channel. This is evident
also from the connection graph used in the semantics of PC, defined below.

5

name of q. Any other process wanting to communicate with q must therefore be
first informed of its existence (as happens, e.g., in object- and service-oriented
computing [13,16]). This is achieved with the introduction term p : q <-> r, read
“p introduces q and r” (with p, q and r distinct). As its double-arrow syntax
suggests, this action represents two communications – one where p sends q’s
name to r, and another where p sends r’s name to q. This will become explicit
in § 4.
In a conditional term if p.e then C1 else C2 , process p evaluates e to choose
between the possible continuations C1 and C2 .
T ) = C defines a procedure
The set D contains global procedures. Term X(qf
X
X with body CX , which can be used anywhere in hD, Ci – in particular, inside
CX . The names q̃ are bound to CX , and they are exactly the free process names
in CX . Each procedure can be defined at most once in D. Term Xhp̃i calls
(or invokes) procedure X by passing p̃ as parameters. Procedure calls inside
definitions must be guarded, i.e., they can only occur after a communication
action.
We work up to α-equivalence in choreographies, assuming the Barendregt
convention. Bound variables are renamed as needed when expanding procedure
calls.
Example 2. Recall procedure MS from our merge sort example in the Introduction
(Example 1). If we annotate the parameter p and the started processes q1 and
q2 with a type, e.g., List(T ) for some T (the type of lists containing elements
of type T ), then MS is a valid procedure definition in PC, as long as we allow
T stands for the sequence
two straightforward syntactic conventions: (i) p start qf
p start qT1 1 ; . . . ; p start qTnn ; (ii) a communication of the form p.e -> q stands for
p.e -> q.id, where id is the identity function: it sets the content of q to the value
received from p. We adopt these conventions also in the remainder.
Remark 1 (Design choices). We comment on two of our design choices.
The introduction action (p : q <-> r) requires a three-way synchronization,
and essentially performs two communications. The alternative development of
PC with asymmetric introduction (an action p : q -> r whereby p sends q’s name
to r, but not conversely) is essentially the same as ours. Since in our examples we
always perform introductions in pairs, the current choice makes the presentation
easier.
The restriction that each process stores only one value of a fixed type is, in
practice, a minor constraint. As shown in Example 2, types can be tuples or lists,
which mimics storing several values. Also, a process can create new processes
with different types – so we can encode changing the type of p by having p create
a new process p′ and then continuing the choreography with p′ instead of p.
Remark 2 (Label Selection). We briefly motivate the need for selections (p -> q[l]).
Consider the choreography if p.coinflip then (p. ∗ -> r) else (r. ∗ -> p). Here, p flips
a coin to decide whether to send a value to r or to receive a value from r. Since
processes run independently and share no data, only p knows which branch of
6

G

p ←→ q e[σ(p)/∗] ↓ v f [σ(q)/∗](v) ↓ w
⌊C|Com⌉
G, p.e -> q.f ; C, σ →D G, C, σ[q 7→ w]
G

p ←→ q
⌊C|Sel⌉
G, p -> q[l]; C, σ →D G, C, σ
G, p start qT ; C, σ →D G ∪ {p ↔ q}, C, σ[q 7→ ⊥T ]
G

⌊C|Start⌉

G

p ←→ q p ←→ r
⌊C|Tell⌉
G, p : q <-> r; C, σ →D G ∪ {q ↔ r}, C, σ
i = 1 if e[σ(p)/∗] ↓ true, i = 2 otherwise
⌊C|Cond⌉
G, (if p.e then C1 else C2 ); C, σ →D G, Ci # C, σ
C1 D C2

G, C2 , σ →D G′ , C2′ , σ ′
G, C1 , σ →D G′ , C1′ , σ ′

C2′ D C1′

⌊C|Struct⌉

Fig. 2. Procedural Choreographies, Semantics.
the conditional will be executed; but this information is essential for r to decide
on its behaviour. To propagate p’s decision to r, we use selections:
if p.coinflip then (p -> r[l]; p. ∗ -> r) else (p -> r[r]; r. ∗ -> p)
Now r receives a label reflecting the choice made by p, and can decide what to
do.
This intuition is formalised by the definition of EndPoint Projection in § 4.
The first choreography above is not projectable, whereas the second one is. See
also Example 5 at the end of this section.
Semantics. We define a reduction semantics →D for PC, parameterised over
D. We model the state of processes with a (total) state function σ, where σ(p)
denotes the value stored in p. We assume that each type T ∈ T has a special
value ⊥T , representing an uninitialised process state. The semantics of PC also
includes a connection graph G, keeping track of which processes know each other.
G
In the rules, p ←→ q denotes that G contains an edge between p and q, and
G ∪ {p ↔ q} denotes the graph obtained from G by adding an edge between p
and q (if missing).
Executing a communication action p.e -> q.f in rule ⌊C|Com⌉ requires that: p
and q are connected in G; e is well typed; and the type of e matches that expected
by the function f at the receiver. The last two conditions are encapsulated in
the notation e ↓ v, read “e evaluates to v”. Choreographies can thus deadlock
(be unable to reduce) because of errors in the programming of communications;
this issue is addressed by our typing discipline in § 3.
Rule ⌊C|Sel⌉ defines selection as a no-op for choreographies (see Remark 2).
7

pn(η) ∩ pn(η ′ ) = ∅
′

′

η; η ≡D η ; η

⌊C|Eta-Eta⌉

0; C D C

pn(I) ∩ pn(I ′ ) = ∅

⌊C|End⌉

I; I ′ ≡D I ′ ; I

⌊C|I-I⌉

pn(I) ∩ pn(η) = ∅
⌊C|I-Eta⌉
η; I ≡D I; η

T) = C
X(qf
X ∈ D
⌊C|Unfold⌉
Xhp̃i; C D CX [p̃/q̃] # C

{p, q} ∩ pn(η) = ∅
⌊C|Eta-Cond⌉
if p.e then (η; C1 ) else (η; C2 ) ≡D η; if p.e then C1 else C2
if p.e then (C1 ; η) else (C2 ; η) ≡D if p.e then C1 else C2 ; η
{p, q} ∩ {r, s} = ∅
if p.e then (if q.e′ then C1 else C2 ) else (if q.e′ then C1′ else C2′ )
≡D
if q.e′ then (if p.e then C1 else C1′ ) else (if p.e then C2 else C2′ )

⌊C|Cond-Eta⌉
⌊C|Cond-Cond⌉

Fig. 3. Procedural Choreographies, Structural precongruence .

Rule ⌊C|Start⌉ models the creation of a process. In the reductum, the starter
and started processes are connected and can thus communicate with each other.
Rule ⌊C|Tell⌉ captures name mobility, by creating a connection between two
processes q and r when they are introduced by a process p that is connected to
both.
Rule ⌊C|Cond⌉ uses the auxiliary operator # to obtain a reductum in the syntax of PC regardless of the forms of the branches C1 and C2 and the continuation
C. Operator # is defined by η#C = η; C, I#C = I; C and (C1 ; C2 )#C = C1 ; (C2 #C).
This operator extends the scope of bound names: any name p bound in C has
its scope extended also to C ′ . This scope extension is capture-avoiding, as the
Barendregt convention guarantees that p is not used in C ′ .
Rule ⌊C|Struct⌉ makes use of the structural precongruence D , which is
defined by the rules in Figure 3. We write C ≡D C ′ when C D C ′ and C ′ D C,
and denote the set of process names (free or bound) in a choreography C by
pn(C). Rule ⌊C|Unfold⌉ unfolds a procedure call, again using the # operator
defined above, and rule ⌊C|End⌉ is garbage collection of 0.
The other rules formalise the notion of implicit parallelism anticipated in
§ 1. Rule ⌊C|Eta-Eta⌉ permutes two communications performed by processes
that are all distinct, modelling that processes run independently of one another.
For example, p. ∗ -> q; r. ∗ -> s ≡D r. ∗ -> s; p. ∗ -> q because these two
communications are non-interfering, but p.∗ -> q; q.∗ -> s 6≡D q.∗ -> s; p.∗ -> q:
since the second communication causally depends on the first (both involve q).
This reasoning is extended to instructions in rule ⌊C|I-I⌉; in particular, two
procedure calls can be swapped if they share no arguments. This is sound because a procedure can only define actions for processes that are either passed
as arguments or started inside of the procedure itself, and the latter cannot
be leaked to the original call site. Thus, any actions obtained by unfolding the
8

first procedure call involve different processes than those obtained by unfolding
the second one. As the example below shows, calls to the same procedure can be
exchanged, since X and Y need not be distinct. The other rules follow similar intuitions; we omit rules ⌊C|I-Cond⌉ and ⌊C|Cond-I⌉, analogous to ⌊C|Eta-Cond⌉
and ⌊C|Cond-Eta⌉.
Example 3. In our merge sort example, rule ⌊C|I-I⌉ allows the recursive calls
MS<q1 > and MS<q2 > to be exchanged. Furthermore, after the calls are unfolded,

implicit parallelism allows their code to be interleaved in any way.
This example exhibits typical map-reduce behaviour: each new process receives its input, runs independently from all others, and then sends its result to
its creator.
Example 4. A more refined example of implicit parallelism involves swapping
communications from procedure calls that share process names. Consider the
procedure
auth (c ,a ,r , l ) = c . creds -> a . rCreds ;
a . chk -> r . res ; a . log -> l . app

Client c sends its credentials to an authentication server a, which stores the
result of authentication in r and appends a log of this operation at process l.
In the choreography auth<c,a1,r1,l>; auth<c,a2,r2,l>, a client c authenticates
at two different authentication servers a1 and a2. After unfolding the two calls,
rule ⌊C|Eta-Eta⌉ yields the following interleaving:
c . creds -> a1 . rCreds ; c . creds -> a2 . rCreds ;
a2 . chk -> r2 . res ; a1 . chk -> r1 . res ;
a1 . log -> l . app ; a2 . log -> l . app

Thus, the two authentications proceed in parallel. Observe that the logging operations cannot be swapped, since they use the same logging process l.
Example 5. A more sophisticated example involves modularly composing different procedures that take multiple parameters. Here, we write a choreography
where a client c downloads a collection of files from a server s. The key idea
is to download all files in parallel via streaming, by having the client and the
server each create subprocesses to handle the transfer of each file. This allows
the client to request and start downloading each file without waiting for previous
downloads to finish.
par_download (c , s ) = if c . more
then c -> s [ more ]; c start c ’; s start s ’;
s : c <-> s ’; c . top -> s ’; pop <c >;
c : c ’ <-> s ’; download <c ’ ,s ’ >;
par_download <c ,s >; c ’. file -> c . store
else c -> s [ end ]

At the start of par_download , the client c checks whether it wants to download
more files and informs the server s of the result via a label selection. In the
9

affirmative case, the client and the server start two subprocesses, c′ and s′ respectively, and the server introduces c to s′ (s: c <-> s’). The client c sends to
s′ the name of the file to download (c.top -> s’) and removes it from its collection, using procedure pop (omitted), afterwards introducing its own subprocess
c′ to s′ . The file download is handled by c′ and s′ (using procedure download),
while c and s continue operating (par_download<c,s>). Finally, c′ waits until c is
ready to store the downloaded file.
Procedure download has a similar structure. It implements a stream where a
file is sequentially transferred in chunks from a process s to another process c.
download (c , s ) = if s . more
then s -> c [ more ]; s . next -> c . append ; pop <s >; download <c ,s >
else s -> c [ end ]

The implementation of par_download exploits implicit parallelism considerably. All calls to download are made with disjoint sets of parameters (processes),
thus they can be fully parallelised by our semantics: many instances of download
run at the same time, each one implementing a (sequential) stream. By implicit parallelism, we effectively end up executing many streaming behaviours in
parallel.
We can even compose par_download with auth, such that we execute the parallel download only if the client can successfully authenticate with an authentication server a. Below, we use the shortcut p -> q̃[l] for p -> q1 [l]; . . . ; p -> qn [l].
auth <c ,a ,r ,l >; if r . ok then r -> c , s [ ok ]; par_download <c ,s >
else r -> c , s [ ko ]

3

Typability and Deadlock-Freedom

We give a typing discipline for PC, to checks that (a) the types of functions and
processes are respected by communications and (b) processes that need to communicate are first properly introduced (or connected). Regarding (b), two processes created independently can communicate only after they receive the names
of each other. For instance, in Example 5, the execution of download<c’,s’> would
get stuck if c’ and s’ were not properly introduced in par_download, since our
semantics requires them to be connected.
Typing judgements have the form Γ ; G ⊢ C ⊲ G′ , read “C is well-typed according to the typings in Γ , and when executed from a connection graph that
contains G it produces a connection graph that includes G′ ”. Typing environments Γ are used to track the types of processes and procedures; they are defined
as: Γ ::= ∅ | Γ, p : T | Γ, X : G ⊲ G′ . A typing p : T states that process p stores
values of type T , and a typing X : G ⊲ G′ records the effect of the body of X on
graph G.
The rules for deriving typing judgements are given in Figure 4. We assume
standard typing judgements for functions and expressions, and write ∗ : T ⊢T
e : T and ∗ : T1 ⊢T f : T2 → T3 meaning, respectively “e has type T assuming
that ∗ has type T ” and “f has type T2 → T3 assuming that ∗ has type T1 ”.
10

G

Γ;G ⊢ 0 ⊲ G
G

p ←→ q

p ←→ q Γ ; G ⊢ C ⊲ G′
⌊T|Sel⌉
Γ ; G ⊢ p -> q[l]; C ⊲ G′

⌊T|End⌉

Γ ⊢ p : Tp , q : Tq

∗ : T p ⊢T e : T 1

Γ ; G ⊢ C ⊲ G′
⌊T|EndSeq⌉
Γ ; G ⊢ 0; C ⊲ G′

∗ : T q ⊢T f : T 1 → T q

Γ ; G ⊢ C ⊲ G′

′

Γ ; G ⊢ p.e -> q.f ; C ⊲ G
Γ ⊢p:T

∗ : T ⊢T e : bool Γ ; G ⊢ Ci ⊲ Gi Γ ; G1 ∩ G2 ⊢ C ⊲ G′
⌊T|Cond⌉
Γ ; G ⊢ (if p.e then C1 else C2 ); C ⊲ G′

Γ, q : T ; G ∪ {p ↔ q} ⊢ C ⊲ G′
T

′

Γ ; G ⊢ p start q ; C ⊲ G

′
T) : G
Γ ⊢ X(qf
X ⊲ GX

G

Γ ⊢ p i : Ti

G

p ←→ q

⌊T|Start⌉

p ←→ r

Γ ; G ∪ {q ↔ r} ⊢ C ⊲ G′

Γ ; G ⊢ p : q <-> r; C ⊲ G′
GX [p̃/q̃] ⊆ G

Γ ; G ∪ (G′X [p̃/q̃]) ⊢ C ⊲ G′

′

Γ ; G ⊢ Xhp̃i; C ⊲ G

Fig. 4. Procedural Choreographies, Typing Rules.

Verifying that communications respect the expected types is straightforward,
using the connection graph G to track which processes have been introduced to
each other. In rule ⌊T|Start⌉, we implicitly use the fact that q does not appear
yet in G, which is another consequence of using the Barendregt convention. The
final graph G′ is only used in procedure calls (rule ⌊T|Call⌉). Other rules leave
it unchanged.
To type a procedural choreography, we need to type its set of procedure
T ) = C ∈ D, there is exactly one
definitions D. We write Γ ⊢ D if: for each X(qf
X
′
f
T
typing X(q ) : GX ⊲GX ∈ Γ , and this typing is such that Γ, q]
: T , GX ⊢ CX ⊲G′X .
′
We say that Γ ⊢ hD, Ci if Γ, ΓD ; GC ⊢ C, G for some ΓD such that ΓD ⊢ D and
some G′ , where GC is the full graph whose nodes are the free process names in C.
The choice of GC is motivated by observing that (i) all top-level processes should
know each other and (ii) eventual connections between processes not occuring
in C do not affect its typability.
Well-typed choreographies either terminate or diverge.3
Theorem 1 (Deadlock freedom and Subject reduction). Given a choreography C and a set D of procedure definitions, if Γ ⊢ D and Γ ; G1 ⊢ C ⊲ G′1
for some Γ , G1 and G′1 , then either:
– C D 0; or,
– for every σ, there exist G2 , C ′ and σ ′ such that G1 , C, σ →D G2 , C ′ , σ ′ and
Γ ′ ; G2 ⊢ C ′ ⊲ G′2 for some Γ ′ ⊇ Γ and G′2 .
(Proofs of theorems can be found in the Appendix.)
3

⌊T|Com⌉

Since we are interested in communications, we assume evaluation of functions and
expressions to terminate on values with the right types (see § 7, Faults).

11

⌊T|Tell⌉

⌊T|Call⌉

Checking that Γ ⊢ hD, Ci is not trivial, as it requires “guessing” ΓD . However, this set can be computed from hD, Ci, entailing type inference properties
for PC.
Theorem 2. Given Γ , D and C, Γ ⊢ hD, Ci is decidable.
Theorem 2 may seem a bit surprising; the key idea of its proof is that typechecking may require expanding recursive definitions, but their parameters only
need to be instantiated with process names from a finite set. With a similar idea,
we also obtain type inference.
Theorem 3. There is an algorithm that, given any hD, Ci, outputs:
– a set Γ such that Γ ⊢ hD, Ci, if such a Γ exists;
– NO, if no such Γ exists.
Theorem 4. The types of arguments in procedure definitions and the types of
freshly created processes can be inferred automatically.
Remark 3 (Inferring introductions). Theorems 3 and 4 allow us to omit type
annotations in choreographies, if the types of functions and expressions at processes are known (from ⊢T ). Thus, programmers can write choreographies as in
our examples.
The same reasoning could be adopted to infer missing introductions (p :
q <-> r) in a choreography automatically, thus lifting the programmer also from
having to think about connections entirely. However, while the types inferred
for a choreography do not affect its behaviour, the placement of introductions
does. In particular, when invoking procedures one is faced with the choice of
adding the necessary introductions inside the procedure definition (weakening
the conditions for its invocation) or in the code calling it (making the procedure
body more efficient).

4

Synthesising Process Implementations

We now present our EndPoint Projection (EPP), which compiles a choreography
to a concurrent implementation represented in terms of a process calculus.
4.1

Procedural Processes (PP)

We introduce our target process model, Procedural Processes (PP).
Syntax. The syntax of PP is given in Figure 5. A term p⊲v B is a process, where
p is its name, v is its value, and B is its behaviour. Networks, ranged over by
N, M , are parallel compositions of processes, where 0 is the inactive network.
Finally, hB, N i is a procedural network, where B defines the procedures that
the processes in N may invoke. Values, expressions and functions are as in PC.
A process executing a send term q!e; B sends the evaluation of expression e
to q, and proceeds as B. Term p?f ; B is the dual receiving action: the process
12

B ::= q!e; B | p?f ; B | q!!r; B | p?r; B | q ⊕ l; B | p&{li : Bi }i∈I ; B
| 0 | start qT ⊲ B2 ; B1 | if e then B1 else B2 ; B | Xhp̃i; B | 0; B
B ::= X(q̃) = B, B | ∅

N, M ::= p ⊲v B | (N | M ) | 0

Fig. 5. Procedural Processes, Syntax.
u = (f [w/∗])(e[v/∗])
⌊P|Com⌉
p ⊲v q!e; B1 | q ⊲w p?f ; B2 →B p ⊲v B1 | q ⊲u B2
j∈I
⌊P|Sel⌉
p ⊲v q ⊕ lj ; B | q ⊲w p&{li : Bi }i∈I →B p ⊲v B | q ⊲w Bj
i = 1 if e[v/∗] = true, i = 2 otherwise
⌊P|Cond⌉
p ⊲v if e then B1 else B2 →B p ⊲v Bi
q′ fresh
p ⊲v (start q ⊲ B2 ; B1 ) →B p ⊲v B1 [q′ /q] | q′ ⊲⊥T B2
T

⌊P|Start⌉

p ⊲v q!!r; B1 | q ⊲w p?r; B2 | r ⊲u p?q; B3 →B p ⊲v B1 | q ⊲w B2 | r ⊲u B3
N →B N ′
⌊P|Par⌉
N | M →B N ′ | M

N B M

M →B M ′
N →B N ′

M ′ B N ′

⌊P|Tell⌉

⌊P|Struct⌉

Fig. 6. Procedural Processes, Semantics.

executing it receives a value from p, combines it with its value as specified by
f , and then proceeds as B. Term q!!r sends process name r to q and process
name q to r, making q and r “aware” of each other. The dual action is p?r,
which receives a process name from p that replaces the bound variable r in the
continuation. Term q⊕l; B sends the selection of a label l to process q. Selections
are received by the branching term p&{li : Bi }i∈I , which can receive a selection
for any of the labels li and proceed according to Bi . Branching terms must offer
at least one branch. Term start q⊲B2 ; B1 starts a new process (with a fresh name)
executing B2 , and proceeds in parallel as B1 . Conditionals, procedure calls, and
termination are standard. Term start q ⊲ B2 ; B1 binds q in B1 , and p?r; B binds
r in B.
Semantics. The rules defining the reduction relation →B for PP are shown in
Figure 6. As in PC, they are parameterised on the set of behavioural procedures
B. Rule ⌊P|Com⌉ models value communication: a process p executing a send
action towards a process q can synchronise with a receive-from-p action at q; in
the reductum, f is used to update the memory of q by combining its contents
with the value sent by p. The placeholder ∗ is replaced with the current value
of p in e (resp. q in f ). Rule ⌊P|Tell⌉ establishes a three-way synchronisation,
13

p ⊲v 0 B 0
0; B B B

⌊P|AZero⌉

⌊P|End⌉

N | 0 B N
f
T
X(q ) = BX ∈ B

⌊P|NZero⌉

Xhp̃i; B B BX [p̃/q̃] # B

⌊P|Unfold⌉

Fig. 7. Procedural Processes, Structural precongruence B .

allowing a process to introduce two others. Since the received names are bound at
the receivers, we rely on α-conversion to make the receivers agree on each other’s
name, as done in session types [17]. (Differently from PC, we do not assume the
Barendregt convention here, in line with the tradition of process calculi.) Rule
⌊P|Sel⌉ is standard selection [17], where the sender process selects one of the
branches offered by the receiver. In rule ⌊P|Start⌉, we require the name of the
created process to be globally fresh. All other rules are standard. Rule ⌊P|Struct⌉
uses structural precongruence B , which is the smallest precongruence satisfying
associativity and commutativity of parallel ( | ) and the rules in Figure 7. Rule
⌊P|Unfold⌉ expands procedure calls. It uses again the # operator, defined as for
PC but with terms in the PP language.
Remark 4. Our three-way synchronisation in rule ⌊P|Tell⌉ could be easily encoded with two standard two-way communications of names, as in the π-calculus [27]
(see also Remark 1). Our choice gives a clearer formulation of EPP.
Example 6. We show a process implementation of the merge sort choreography
in Example 1 from § 1. All processes are annotated with type List(T ) (omitted);
id is the identity function (Example 2).
MS p ( p ) = if is_small then 0
else start q 1 ⊲ ( p ? id ; MS p <q 1 >; p !*);
start q 2 ⊲ ( p ? id ; MS p <q 2 >; p !*);
q 1 ! split 1 ; q 2 ! split 2 ; q 1 ? id ; q 2 ? merge

In the next section, we show that our EPP generates this process implementation
automatically from the choreography in Example 1.
4.2

EndPoint Projection (EPP)

We now show how to compile programs in PC to processes in PP.
Behaviour Projection. We start by defining how to project the behaviour of
a single process p, a partial function denoted [[C]]p . The rules defining behaviour
projection are given in Figure 8. Each choreography term is projected to the local
action of the process that we are projecting. For example, a communication term
p.e -> q.f projects a send action for the sender p, a receive action for the receiver
q, or skips to the continuation otherwise. The rules for projecting a selection or
an introduction (name mobility) are similar.
14



q!e; [[C]]r
[[p.e -> q.f ; C]]r = p?f ; [[C]]r


[[C]]r



q ⊕ l; [[C]]r
[[p -> q[l]; C]]r = p&{l : [[C]]r }


[[C]]r

if r = p
if r = q
otherwise


q!!r; [[C]]s




p?r; [[C]]s
[[p : q <-> r; C]]s =

p?q; [[C]]s



[[C]]s

if r = p
if r = q
otherwise

(
if s = p
Xi hp̃i; [[C]]r if r = pi
[[Xhp̃i; C]]r =
if s = q
[[C]]r
otherwise
if s = r
[[0]]r = 0
[[0; C]]r = [[C]]r
otherwise
(
if e then [[C1 ]]r else [[C2 ]]r ; [[C]]r if r = p
[[if p.e then C1 else C2 ; C]]r =
([[C1 ]]r ⊔ [[C2 ]]r ); [[C]]r
otherwise
(
start q ⊲ [[C]]q ; [[C]]r if r = p
[[p start qT ; C]]r =
[[C]]r
otherwise

Fig. 8. Procedural Choreographies, Behaviour Projection.
The rule for projecting a conditional uses the partial merging operator ⊔:
B ⊔ B ′ is isomorphic to B and B ′ up to branching, where the branches of B or
B ′ with distinct labels are also included. The interesting rule defining merge is:
(p&{li : Bi }i∈J ; B) ⊔ (p&{li : Bi′ }i∈K ; B ′ ) =


p& {li : (Bi ⊔ Bi′ )}i∈J∩K ∪ {li : Bi }i∈J\K ∪ {li : Bi′ }i∈K\J ; (B ⊔ B ′ )

The idea of merging comes from [5]. Here, we extend it to general recursion,
parametric procedures, and process starts. The complete definition of merging
is given in the Appendix. Merging allows the process that decides a conditional
to inform other processes of its choice later on, using selections. It is found
repeatedly in most choreography models [5,9,19].
Building on behaviour projection, we define how to project the set D of
procedure definitions. We need to consider two main aspects. The first is that,
at runtime, the choreography may invoke a procedure X multiple times, but
potentially passing a process r at different argument positions each time. This
means that r may be called to play different “roles” in the implementation of
the procedure. For this reason, we project the behaviour of each possible process
parameter p as the local procedure Xp . The second aspect is: depending on the
role that r is called to play by the choreography, it needs to know the names of
the other processes that it is supposed to communicate with in the choreographic
procedure. We deal with this by simply passing all arguments, which means that
some of them may even be unknown to the process invoking the procedure. This
is not a problem: we focus on typable choreographies, and typing ensures that
those parameters are not actually used in the projected procedure (so they act as
“dummies”). We do this for clarity, since it yields a simpler formulation of EPP.
In practice, we can annotate the EPP by analysing which parameters of each
15

recursive definition are actually used in each of its projections, and instantiating
only those (see Appendix).
We can now define
o
[n
f
T ) = C]] | X(q
T) = C ∈ D
[[D]] =
[[X(qf
T = qT1 , . . . , qTn ,
where, for qf
n
1

T ) = C]] = {X (q̃) = [[C]] , . . . , X (q̃) = [[C]] } .
[[X(qf
n
qn
1
q1

Definition 1 (EPP). Given a procedural choreography hD, Ci and a state σ,
the endpoint projection [[D, C, σ]] is the parallel composition of the processes in
C with all definitions from D:
E
D
Q
[[D, C, σ]] = h[[D]], [[C, σ]]i = [[D]], p∈pn(C) p ⊲σ(p) [[C]]p
where [[C, σ]], the EPP of C wrt state σ, is independent of D.
Since the σs are total, if [[C, σ]] is defined for some σ, then [[C, σ ′ ]] is defined
also for all other σ ′ . When [[C, σ]] = N is defined for any σ, we say that C is
projectable and that N is the projection of C, σ. Similar considerations apply to
[[D, C, σ]].
Example 7. The EPP of the choreography in Example 1 is given in Example 6.
Example 8. We give a more sophisticated example involving merging and introductions: the projection of procedure par_download (Example 5) for process s.
(We omit the type annotations.)
par_download s (c , s ) = c &{
more : start s ’ ⊲ ( s ? c ; c ? id ; c ?c ’; download s <c ’ ,s ’ >);
c !! s ’; par_download s <c ,s >
end : 0
}

Observe that we call procedure downloads , as s’ occurs in the position of that
procedure’s formal argument s.
Properties. EPP guarantees correctness by construction: the code synthesised
from a choreography follows it precisely.
Theorem 5 (EPP Theorem). If hD, Ci is projectable, Γ ⊢ D, and Γ ; G ⊢
C ⊲ G∗ , then, for all σ:
– (Completeness) if G, C, σ →D G′ , C ′ , σ ′ , then [[C, σ]] →[[D]] ≻ [[C ′ , σ ′ ]];
– (Soundness) if [[C, σ]] →[[D]] N , then G, C, σ →D G′ , C ′ , σ ′ for some G′ , σ ′
such that [[C ′ , σ ′ ]] ≺ N .
Above, the pruning relation ≺ from [5] eliminates the branches introduced by
the merging operator ⊔ when they are not needed anymore to follow the originating choreography (we write N ≻ N ′ when N ′ ≺ N ). Pruning does not alter
reductions, since the eliminated branches are never selected [5]. Combining Theorem 5 with Theorem 1 we get that the projections of typable PC terms never
deadlock.
16

Corollary 1 (Deadlock-freedom by construction). Let N = [[C, σ]] for
some C and σ, and assume that Γ ; G ⊢ C ⊲ G′ for some Γ such that Γ ⊢ D and
some G and G′ . Then, either:
– N [[D]] 0 (N has terminated);
– or there exists N ′ such that N →[[D]] N ′ (N can reduce).
Remark 5 (Amendment). A choreography in PC can only be unprojectable because of unmergeable subterms. Thus, every choreography can be made projectable by only adding label selections. This can be formalized in an amendment
algorithm, as in other choreography languages [20,11], reported in the Appendix.
For example, the first (unprojectable) choreography in Remark 2 can be amended
to the projectable choreography presented at the end of the same remark.
In practice, the same argument as for inferring introduction terms (Remark 3)
applies. Although amendment allows us to write choreographies without worrying about label selections, it is useful to give the programmer the option to place
them where most convenient. For example, consider a process p making an internal choice that affects processes q and r. If one of these two processes has to
perform a slower computation in response to that choice, then it makes sense
for p to send a label selection to it first, and only afterwards to notify the other
process.

5

Asynchrony

We define an alternative semantics to PC and PP, whereby communication becomes asynchronous. We show that the results stated in the previous sections
also hold for the asynchronous case.
5.1

Asynchronous PC (aPC)

Syntax. In asynchronous PC (aPC), communications are not atomically executed anymore, but consist of multiple actions. In particular, the sender of a
message can proceed in its execution without waiting for the receiver to receive
such message.
The intuition behind aPC is that the language is extended with new runtime terms that capture this refinement of execution steps.4 At runtime communications are expanded into multiple actions. For example, a communication
x
x
p.e -> q.f expands in p.e -> •q – a send action from p – and •p -> q.f – a
receive action by q. The process subscripts at • are immaterial for the semantics
of aPC, but are useful for the definition of EPP. The tag x specifies that, in the
original choreography, that message from p should reach that receive action at
x
q. Executing p.e -> •q replaces x in the corresponding receive action with the
4

Recall that runtime terms are assumed never to be used by programmers (like term
0; C in PC). They are used only to represent runtime states.

17

v̂

x

x,y

l̂

x

p̂

η ::= . . . | p.e -> •q | •p -> q.f | p -> •q [l] | •p -> q[l] | p : •q <-> •r | •p .r -> q
v̂ ::= x | v

l̂ ::= x | l

p̂ ::= x | p

Fig. 9. Asynchronous PC, Syntax of New Runtime Terms.
v

v

actual value v computed from e at p, yielding •p -> q.f ; executing •p -> q.f
updates the state of q.
We now define aPC formally. The new terms are given in Figure 9, and they
are all runtime terms. The terms follow the intuition given for value communications, extended to selection and introduction. Label selection expands in
x,y

l̂

x

p -> •q [l] and •p -> q[l], and introduction expands in p : •q <-> •r and two
p̂

•p .r -> q actions. The tags in these actions are not essential for propagating
values as above, but they make the treatment of all new actions similar. Process
names for the new runtime terms are defined as follows, ignoring process names
in tags and in • subscripts.
x

x,y

x

pn(p.e -> •q ) = pn(p -> •q [l]) = pn(p : •q <-> •r ) = {p}
v̂

p̂

l̂

pn(•p -> q.f ) = pn(•p -> q[l]) = pn(•p .r -> q) = {q}
Semantics. The interplay between asynchronous communications and name
mobility requires the connection graph to be directed in aPC, since the processes
q and r in an introduction term p : q <-> r may receive names at different times
G
now. An edge from p to q in G, denoted q → p, now means that p knows q’s
name – so p is able to send messages to q or to listen for incoming messages
from q.
The semantics for aPC includes:
– the rules from Figure 10, which are the asynchronous counterpart to ⌊C|Com⌉
in PC, and similar rules for selection and introduction;
– rules ⌊C|Cond⌉ and ⌊C|Struct⌉ from PC;
– rule ⌊C|Start⌉ from PC, where G ∪{p ↔ q} is the graph obtained by adding
the two directed edges between p and q to G;
– the rules defining D (Figure 3), with η now ranging over all communication
actions in aPC;
– the new rules for D in Figure 11.
The missing new rules are given in the Appendix. By the Barendregt convention,
tags introduced by the rules in Figure 11 are globally fresh. Thus, they maintain
the correspondence between the value being sent and that being received.
The key to the semantics of aPC lies in the new swaps allowed by D , due
to the definition of pn for the new terms. This captures the concurrency that
arises from asynchronous communications.
18

G

p→q

e[σ(p)/∗] ↓ v

⌊C|Com-S⌉

x

G, p.e -> •q ; C, σ →D G, C[v/x], σ
G

q→p

f [σ(q)/∗](v) ↓ w

⌊C|Com-R⌉

v

G, •p -> q.f ; C, σ →D G, C, σ[q 7→ w]

Fig. 10. Asynchronous PC, Semantics of New Runtime Terms.

x

x

⌊C|Com-U⌉

x

⌊C|Sel-U⌉

p.e -> q.f D p.e -> •q ; •p -> q.f
x

p -> q[l] D p -> •q [l]; •p -> q[l]
x,y

y

x

⌊C|Tell-U⌉

p : q <-> r D p : •q <-> •r ; •p .r -> q; •p .q -> r

Fig. 11. Asynchronous PC, Structural Precongruence (New Additional Rules).
Example 9. Let C be p.e -> q.f ; p.e′ -> r.f ′ . To execute C in aPC, we expand
it:
y
y
x
x
C D p.e -> •q ; •p -> q.f ′ ; p.e′ -> •r ; •p -> r.f ′
Using D , we can swap the second term to the end (it shares no process names
with the subsequent terms according to pn):
C

D

y

y

x

x

p.e -> •q ; p.e′ -> •r ; •p -> r.f ′ ; •p -> q.f ′

Now p can send both messages immediately, and r can receive its message before q.
Example 10. Due to asynchrony, a process q can now send a message to another
process r that does not yet know about q. However, r is still unable to receive
G
G
it before learning q’s name, as expected [27]. Assume that p ←→ q and p ←→ r
∆
and consider the choreography: C = p : q <-> r; q. ∗ -> r.f . We can unfold C to
C

D

x,y

y

x

x

z

p : •q <-> •r ; •p .r -> q; •p .q -> r; q.∗ -> •r ; •q -> r.f

and, by D , swap the third and fourth term
C

D

x,y

x

z

y

x

p : •q <-> •r ; •p .r -> q; q.∗ -> •r ; •p .q -> r; •q -> r.f

which corresponds to an execution path where q sends its contents to r before
r is notified of q’s name. The last two actions can not be swapped, so r cannot
access q’s message before receiving its name.
19

G

p→q

Γ ⊢ p : Tp

Γ ⊕ (x : T ); G ⊢ C ⊲ G′

∗ : T p ⊢T e : T
x

Γ ; G ⊢ p.e -> •q ; C ⊲ G′
G

q→p

Γ ⊢ q : Tq

∗ : T q ⊢T f : T → T q

⌊T|Com-S⌉

Γ ⊕ (x : T ); G ⊢ C ⊲ G′

x

Γ ; G ⊢ •p -> q.f ; C ⊲ G′
G

q→p

Γ ⊢ q : Tq

⊢T v : T

∗ : T q ⊢T f : T → T q

⌊T|Com-RV⌉

Γ ; G ⊢ C ⊲ G′

v

Γ ; G ⊢ •p -> q.f ; C ⊲ G′

⌊T|Com-RT⌉

Fig. 12. Asynchronous PC, Typing Rules (New Runtime Terms).

To restate Theorems 1–4 for aPC, we extend our type system to the new
runtime terms. In particular, we augment contexts Γ to contain also type declarations for tags (x : T ) and assignments of labels or process identifiers to tags
(x = l or x = p). The type system of aPC contains the rules for PC (Figure 4)
together with the new rules given in Figure 12 and analogous ones for selections
and introductions. Furthermore, in rule ⌊T|End⌉ (from PC) we require that Γ
does not contain any assertions x : T or x = t, meaning that there should be no
dangling actions.
The context Γ ⊕ (x : T ) used in the rules is defined below; the interpretation
of Γ ⊕ (x = t) is similar. The operator ⊕ is partial. In particular, any judgement
involving Γ ⊕ (x : T ) is false if Γ already declares x with a different type.


if x is not declared in Γ
Γ, x : T
Γ ⊕ (x : T ) = Γ \ {x : T } if x : T ∈ Γ


undefined
otherwise
Thus, typing a receiving action depends on whether or not it corresponds to a
message that has already been sent according to Γ .
If we consider only program choreographies (without runtime terms), then
the typing systems for aPC and PC coincide (as the connection graph is always
symmetric); in particular, Theorems 2–4 automatically hold for program choreographies in aPC. The proofs of these results, as well as that of Theorem 1, can
be readily adapted to aPC, as the new cases do not pose any difficulty.
PC and aPC enjoy the following operational correspondence.
Theorem 6. For any C in PC, connection graph G, and state σ:
– If G, C, σ →D G′ , C ′ , σ ′ (in PC), then G, C, σ →∗D G′ , C ′ , σ ′ (in aPC).
– If G, C, σ →D G′ , C ′ , σ ′ (in aPC), then there exist C ′′ , G′′ and σ ′′ such that
G, C, σ →D G′′ , C ′′ , σ ′′ (in PC) and G′ , C ′ , σ ′ →∗D G′′ , C ′′ , σ ′′ (in aPC).
In particular, the sequence of messages from a process p to another process q is
received by q in exactly the same order as it is sent by p. Thus, our semantics
20

ρ′q = ρq · hp, e[v/∗]i
ρ

ρ

ρ

ρ′

⌊P|Com-S⌉

p ⊲vp q!e; Bp | q ⊲wq Bq →B p ⊲vp Bp | q ⊲wq Bq
ρq  hp, vi · ρ′q
q

ρ
⊲wq

u = (f [w/∗])(v)
ρ′

⌊P|Com-R⌉

p?f ; B →B q ⊲uq B

Fig. 13. Asynchronous Procedural Processes, Semantics (New Rules).
matches an interpretation of asynchrony supported by queues between processes,
as we make evident in the asynchronous version of PP below.
5.2

Asynchronous PP (aPP)

Syntax. The asynchronous variant of PP, aPP, is easier to define, as the underlying language is almost unchanged. The only syntactic difference is that processes
now have the form p ⊲ρv B, where ρ is a queue of incoming messages. A message
is a pair hq, mi, where q is the sender process and m is a value, label, or process
identifier.
Semantics. The semantics of aPP consists of rules ⌊P|Cond⌉, ⌊P|Par⌉, ⌊P|Cond⌉,
and ⌊P|Start⌉ from PP (Figure 6) together with the rules given in Figure 13 and
analogous variants for selection and introduction (see Appendix). In the reductum of ⌊P|Start⌉, the newly created process is initialized with an empty queue.
Structural precongruence for aPP is defined exactly as for PP. We write ρ·hq, mi
to denote the queue obtained by appending message hq, mi to ρ, and hq, mi · ρ
for the queue with hq, mi at the head and ρ as tail. We simulate having one
separate queue for each other process by allowing incoming messages from different senders to be exchanged, which we represent using the congruence ρ  ρ′
defined by the rule hp, mi · hq, m′ i  hq, m′ i · hp, mi if p 6= q.
All behaviours of PP are valid also in aPP.
Theorem 7. Let N be a PP network. If N →B N ′ (in PP), then N[] →∗B N[]′
(in aPP), where N[] denotes the asynchronous network obtained by adding an
empty queue to each process.
The converse is not true, so the relation between PP and aPP is not so
strong as in Theorem 6 for PC and aPC. This is because of deadlocks: in PP,
a communication action can only take place when the sender and receiver are
ready to synchronize; in aPP, a process can send a message to another process,
even though the intended recipient is not yet able to receive it. For example, the
network p ⊲v q!∗ | q ⊲w 0 is deadlocked in PP but not in aPP.
5.3

EndPoint Projection (EPP) from aPC to aPP

Defining an EPP from aPC to aPP requires extending the previous definition
with clauses for the new runtime terms. The most interesting part is gener21

ating the local queues for each process: when compiling •p .v -> q.f , for example, we need to add hp, vi at the top of q’s queue. However, if we follow
this intuition, Theorem 5 no longer holds for arbitrary aPC choreographies.
This happens because we can write choreographies that use runtime terms in a
“wrong” way, and these are not correctly compiled to aPP. Consider the chore2

ography C = p.1 -> q.f ; •p -> q.f . If we naively project it for some σ, we obtain
hp,2i
[]
p ⊲σ(p) q!1 | q ⊲σ(q) p?f ; p?f , where [] is the empty queue, and q will receive 2
before 1.
To avoid this undesired behaviour, we recall that runtime terms should not
be used by the programmer and restrict ourselves to well-formed choreographies:
those that can arise from executing a choreography that does not contain runtime
terms (i.e., a program).
Definition 2 (Well-formedness). A choreography C in aPC is well-formed if
C R # C P C  C where:
–  is structural precongruence without rule ⌊C|Unfold⌉;
v
– C R only contains unmatched and instantiated receive actions: •p -> q.f ,
l

r

•p -> q[l], •p .r -> q;
– C P C is a PC choreography.
T ) = C is well-formed if C does not contain any runtime acA procedure X(qf
tions. A procedural choreography hD, Ci is well-formed if all procedures in D are
well-formed and C is well-formed.

Well-formedness is decidable, since the set of choreographies equivalent up to 
is decidable. More efficiently, one can check that C is well-formed by swapping all
runtime actions to the beginning and folding all paired send/receive terms. Furthermore, choreography execution preserves well-formedness. The problematic
choreography described above is not well-formed.
Definition 3 (EPP from aPC to aPP). Let hD, Ci be in aPC and σ be a
state. The EPP of hD, Ci and σ is defined as
D
E
Q
(|C|)
[[D, C, σ]] = h[[D]], [[C, σ]]i = [[D]], p∈pn(C) p ⊲σ(p)p [[C]]p
where [[C]]p is defined as for PC (Figure 8) with the extra rules in Figure 14 and
(|C|)p is defined by the rules in Figure 15. The similar rules for selection and
introduction are defined in the Appendix.
In the last case of the definition of (|C|)p (bottom-right), η and I range over
all cases that are not covered previously. The rule for the conditional may seem a
bit surprising: in the case of projectable choreographies, mergeability and wellformedness together imply that unmatched receive actions at a process must
occur in the same order in both branches. Note that projection of choreographies
l′

with ill-formed runtime terms (e.g., •p -> q[l] with l 6= l′ , which cannot occur in
a well-formed choreography) is not defined.
With this definition, we can restate Theorem 5 for aPC and aPP.
22

x

[[p.e -> •q ; C]]r =

(

q!e; [[C]]r
[[C]]r

if r = p
otherwise

v̂

[[•p -> q.f ; C]]r =

(

p?f ; [[C]]r
[[C]]r

if r = q
otherwise

Fig. 14. Asynchronous PC, Behaviour Projection (New Rules).

v

(|•p -> q.f ; C|)r =

(

hp, vi · (|C|)r
(|C|)r

if r = q
otherwise

(|if p <= q then C1 else C2 ; C|)r = (|C1 |)r · (|C|)r
(|η; C|)r = (|I; C|)r = (|C|)r

Fig. 15. Asynchronous PC, State Projection.

Theorem 8 (Asynchronous EPP Theorem). If hD, Ci in aPC is projectable
and well-formed, Γ ⊢ D, and Γ ; G ⊢ C ⊲ G∗ , then, for all σ:
– (Completeness) if G, C, σ →D G′ , C ′ , σ ′ , then [[C, σ]] →[[D]] ≻ [[C ′ , σ ′ ]];
– (Soundness) if [[C, σ]] →[[D]] N , then G, C, σ →D G′ , C ′ , σ ′ for some G′ , σ ′
such that [[C ′ , σ ′ ]] ≺ N .
As a consequence, Corollary 1 applies also to the asynchronous case: the processes projected from aPC into aPP are deadlock-free.

6

Language Extensions

We sketch two simple extensions that enhance the expressivity of (synchronous
and asynchronous) PC without affecting its underlying theory: they only require
simple modifications, and all the results from the previous sections still hold.
Parameter Lists. Our first extension allows procedure parameters to be lists
of processes, on which procedures can then act uniformly by recursion. Formally,
a procedure parameter can now be either a process or a list of processes all with
the same type. We restrict the usage of such lists to the arguments of procedure
calls; however, they may be manipulated by means of pure total functions that
take a list as their only argument. For example, if procedure X takes a list P as
an argument, then X’s body may call other procedures on P , head(P ) or tail(P ),
but it may not include a communication involving head(P ) and another process.
The semantics is extended with a new garbage collection rule: Xh[]i D 0,
i.e., calling a procedure with an empty list is equivalent to termination (0).
In order to type procedures that take process lists as arguments, in a typing
X : G ⊲ G′ we allow the vertices of G and G′ to be not only processes, but also
(formal) lists. This requires adjusting the premise of ⌊T|Call⌉ to the case when
some of the arguments are lists. For when a concrete list is given as argument, we
update the premise GX [p̃/q̃] ⊆ G to check that: if GX contains an edge between
two process lists P and Q, then G must contain edges between p and q for each p
23

in the list supplied for P and each q in the list supplied for Q. The interpretation
of an edge between an argument process and an argument list is similar.
We extend EPP to this enriched language by similarly extending the syntax
of PP and adding the rule q ⊲v Xhp̃i D q ⊲v 0 if q 6∈ p̃. Although we cannot
call procedures with parameter lists based on the result of a conditional without
changing PP (in particular, due to the definition of merge), in this language we
can write more sophisticated examples. In [10], we show how to implement Quicksort, Gaussian elimination and the Fast Fourier Transform in PC, and discuss
how implicit parallelism yields efficient implementations of these algorithms.
Procedures with Holes. The second extension allows the presence of holes in
procedure definitions. Holes are denoted h , where h is a unique name for the
hole in the procedure. Procedure calls are then allowed to specify a choreography
to inject in each hole by means of the syntax Xhp̃i with [hi 7→ Ci ]i where each Ci
is a choreography (in particular, it can be another procedure call) with pn(Ci ) ⊆
p̃. We assume unspecified holes to be filled with 0.
T ) : G ⊲ G′ with {h :
The typing of procedure definitions is extended to X(qf
i
Gi }i , where Gi is the guaranteed connection graph when reaching hole hi .
The remaining adaptations (syntax and semantics of PC and PP, and EPP) are
trivial.
Example 11. Holes enable higher-order composition of choreographies. Consider
the following exchange procedure:
exchange (p ,q ,r , s ) = p . item -> q . get ; h1; r . item -> s . get ; h2

We can either leave the holes empty, or use them to perform some extra actions,
e.g., inserting a payment:
exchange <p ,q ,r ,s > with h1 7→ pay <p ,q > , h2 7→ pay <r ,s >

We can even insert new causal dependencies between the two communications
in exchange, e.g., using q as a broker:
exchange <p ,q ,r ,s > with h1 7→ q . item -> r . get

Using holes, we can also define a general-purpose iterator (see Appendix).

7

Discussion, Future and Related Work

Design of PC. PC is part of a long-term research effort motivated by empirical
studies on concurrency bugs, such as the taxonomies [22] and [21]. They distinguish between deadlock and non-deadlock bugs. In distributed systems, both are
mostly caused by the wrong composition of different protocols, rather than the
wrong implementation of single protocols. Deadlocks are prevented in PC (Corollary 1). Non-deadlock bugs are more subtle, and typically due to the informal
specification (or lack thereof) of the programmer’s intentions wrt protocol composition, which leads to unexpected bad executions. In PC, the programmer’s
24

intentions are formalised as a choreography and the composition of procedures
in code. Synthesis (EPP) guarantees that these intentions are respected (Theorem 5). Typical non-deadlock bugs include lack of causality between messages,
or between an internal computation and a message [21]. For example, a client
may forget to wait for an authentication protocol to complete and include the
resulting security key in its request to a server in another protocol. We can formalise the correct scenario in PC using our auth procedure from Example 4 (c
is the client and s is the server):
auth <c ,a ,r ,l >;
if r . ok then r -> c , s [ ok ];
r . key -> c . addKey ; request <c ,s >
else r -> c , s [ ko ]

There is still ground to be covered to support all the features (e.g., preemption [21]) used in some of the programs included in these empirical studies.
Thus, this kind of studies will also be important for future developments of PC.
Multiparty Session Types. In Multiparty Session Types (MPST) [18], global
types are specifications of single protocols, used for verifying the code of manuallywritten implementations in process models. Global types are similar to a simplified fragment of PC, obtained (among other restrictions) by replacing expressions and functions with constants (representing types), removing process
creation (the processes are fixed), and restricting recursion to parameterless tail
recursion.
MPST leaves the composition of protocols as an implementation detail to the
implementors of processes. As a consequence, protocol compositions may lead
to deadlocks, unlike in PC. We illustrate this key difference with an example,
using our syntax. Consider the protocols X(r, s) = r.e -> s.f and Y (r′ , s′ ) =
r′ .e′ -> s′ .f ′ , and assume that we want to compose their instantiations Xhp, qi
and Y hq, pi. According to MPST, a valid implementation (paraphrased in PP)
is p ⊲v q?f ′ ; q!e | q ⊲v p?f ; p!e′ . Although this network is obviously deadlocked,
this is not detected by MPST because the interleaving of the two protocols
is not checked. In PC, we can only obtain correct implementations, because
compositions are defined at the level of choreographies, e.g., Xhp, qi; Y hq, pi or
Y hq, pi; Xhp, qi.
The authors of [9] augment MPST with a type system that prevents protocol
compositions that may lead to deadlocks, but their approach is too restrictive
when actions from different protocols are interleaved. Consider the following
example, reported as untypable but deadlock-free in [9] (adapted to PC).
X (p , q ) = p .* -> q ; h1; q .* -> p ; p .* -> q ; h2
X <p ,q > with h1 7→ q .* -> p ; p .* -> q , h2 7→ q .* -> p

This code is both typable and projectable in PC, yielding a correct implementation.
Another technique for deadlock-freedom in MPST and similar models is to
restrict connections among processes participating in different protocols to form
25

a tree [4,6,8]. PC is more expressive, since connections can form an arbitrary
graph.
Recent work investigated how to extend MPST to capture protocols where
the number of participants in a session is fixed only at runtime [30], or can grow
during execution [15]. These results use ad-hoc primitives and “middleware”
terms in the process model, e.g., for tracking the number of participants in a
session [15]. Such machinery is not needed in PC. The authors of [14] propose a
theory of nested MPST, which partially recalls our notion of parametric procedures. Differently from PC, procedures are invoked by a coordinator (requiring
extra communications), and compositions of such nested types can deadlock.
Choreographic Programming. None of the examples in this work can be
written in previous models for choreographic programming, which lack full procedural abstraction. As far as we know, this is also the first work exploring
choreographic programming in a general setting, instead of in the context of
web services [5,7,29].
The models in [5,7] are based on choreographic programming and thus support deadlock-freedom even when multiple protocols are used. However, these
models do not support general recursion and parametric procedures, both of
which are novel in this work. Composition and reusability in these models are
thus limited: procedures cannot have continuations; there can only be a limited number of protocols running at any time (modulo dangling asynchronous
actions); and the process names used in a procedure are statically determined,
preventing reuse. In PC, all these limitations are lifted.
Asynchronous communications in choreographic programming were addressed
in [7] using an ad-hoc transition rule. Our approach in aPC, which builds on implicit parallelism, is simpler and yields an EPP Theorem (Theorem 8) that states
a lockstep correspondence between the programmer’s choreography and the synthesised implementation. Instead, in [7], EPP guarantees only a weaker and more
complex confluence correspondence.
Holes in PC recall adaptation scopes for choreographies in [12], used to pinpoint where runtime adaptation of code can take place. However, that work deals
only with choreographies with a finite number of processes.
A major distinguishing feature of PC is the management of connections
among processes, using graphs that are manipulated at runtime. Channel delegation in choreographies [7] behaves in a similar way, but it is less expressive:
a process that introduces two other processes cannot communicate with them
thenceforth without requiring a new auxiliary channel.
Other paradigms. Reo is another approach that, like PC, disentangles computation from communication and focuses on the programming of interactions,
rather than the actions that implement them. In Reo, protocols are obtained by
composing (graphical) connectors, which mediate communications among components [1]. As such, Reo produces rather different and more abstract artifacts
than PC, which require additional machinery to be implemented (a compiler
from Reo to Java uses constraint automata [2]). Programs in PC can be implemented rather directly via standard send and receive primitives (which is
26

typical of choreographies [7]). PC also supports dynamic creation of processes
and guarantees deadlock-freedom by construction, through its simple type system and EPP. Reo supports many interesting connectors and compositions (e.g.,
multicast), which would be interesting to investigate in PC.
In a different direction, there have been proposals of integrating communication protocols (given as session types) with functional programming [28]. These
approaches allow parallel computations of functions to synchronise and exchange
values. As for MPST, protocol compositions are left to the programmer, and the
same limitations discussed for MPST apply.
Local concurrency. Some choreography models support an explicit parallel
operator, e.g., C | C ′ . We chose not to present it here to keep our model simple,
as most behaviours of C | C ′ are captured by implicit parallelism and asynchrony in PC. For example, Xhp, qi | Y hr, si is equivalent to Xhp, qi; Y hr, si in
PC (Rule ⌊C|I-I⌉, Figure 3). However, when some processes names are shared in
the parallel composition, then the parallel operator is more expressive, because
it allows for local concurrency. As an example, consider Xhp, qi | Y hp, si: here, p
is doing more actions concurrently. In PC, we can encode this by spawning new
processes, e.g. our example would become p start r; p : r <-> s; Xhp, qi; Y hr, si. The
price we pay is the extra communications to introduce r (p’s new process) to s
(plus, we may need to send p’s value to r, and maybe send r’s value to p after Y
terminates).
If local concurrency in PC is desired, there are different options for introducing it. A straightforward one is to adapt the parallel operator from [5,18], which,
however, abstracts from how local concurrency is implemented. A more interesting strategy would be to support named local threads in processes. Threads
would share the process location, such that they can receive at the same name
without the need to be introduced. Then, implicit parallelism would allow for
swapping actions at threads (not just processes) with distinct names. Threads
at the same process should not receive from the same sender process at the
same time, to avoid races, which can be prevented via typing (cf. [5]). Integration with separation logic [26] would also be interesting, to allow threads also to
safely share data.
Sessions, Connections, and Mobility. All recent theories based on session
types (e.g., [5,7,8,9,18]) assume that all processes in a session (a protocol execution) have a private full-duplex channel to communicate with each other in that
session. This amounts to requiring that the graph of connections among processes
in a protocol is always complete. This assumption is not necessary in PC, since
our semantics and typing require only the processes that actually communicate
to be connected. This makes PC a suitable model for reasoning about different
kinds of network topologies. In the future, it would be interesting to see whether
our type system and connection graphs can be used to enforce pre-defined network structures (e.g., hypercubes or butterflies), making PC a candidate for the
programming of choreographies that account for hardware restrictions.
Another important aspect of sessions is that each new protocol execution
requires the creation of a new session (and all the connections among its par27

ticipants!). By contrast, protocol executions (running procedures) in PC can
reuse all available connections – allowing for more efficient implementations. We
use this feature in our parallel downloader example (Example 5), where c’ can
still communicate with c even after the latter introduced it to s’. Also, aPC
supports for the first time the asynchronous establishment of new connections
among processes.
The standard results of communication safety found in session-typed calculi
can be derived from our EPP Theorem (Theorem 5), as discussed in [7].
Faults. Some interesting distributed bugs [21] are triggered by unexpected fault
conditions at nodes, making such faults an immediate candidate for the future
developments of PC. Useful inspiration to this aim may be provided by [3].
We have also abstracted from faults and divergence of internal computations:
in PC, we assume that all internal computations terminate successfully. If we
relax these conditions, deadlock-freedom can still be achieved simply by using
timeouts and propagating faults through communications.
Integration. Sometimes, the code synthesised from a choreography has to be
used in combination with legacy process code. For example, we may want to
use an existing authentication server in our auth procedure in Example 4. This
issue is addressed in [24] by using a type theory based on sessions. We leave an
adaptation of this idea in our setting to future work.

28

References
1. Farhad Arbab. Reo: a channel-based coordination model for component composition. Mathematical Structures in Computer Science, 14(3):329–366, 2004.
2. Farhad Arbab, Christel Baier, Jan J. M. M. Rutten, and Marjan Sirjani. Modeling
component connectors in reo by constraint automata: (extended abstract). Electr.
Notes Theor. Comput. Sci., 97:25–46, 2004.
3. Sara Capecchi, Elena Giachino, and Nobuko Yoshida. Global escape in multiparty
sessions. Mathematical Structures in Computer Science, 26(2):156–205, 2016.
4. Marco Carbone and Søren Debois. A graphical approach to progress for structured
communication in web services. In Proc. of ICE’10, 2010.
5. Marco Carbone, Kohei Honda, and Nobuko Yoshida. Structured communicationcentered programming for web services. ACM Trans. Program. Lang. Syst., 34(2):8,
2012.
6. Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Schürmann, and Philip
Wadler. Coherence generalises duality: a logical explanation of multiparty session
types. In CONCUR, 2016. To appear.
7. Marco Carbone and Fabrizio Montesi. Deadlock-freedom-by-design: multiparty
asynchronous global programming. In R. Giacobazzi and R. Cousot, editors,
POPL, pages 263–274. ACM, 2013.
8. Marco Carbone, Fabrizio Montesi, Carsten Schürmann, and Nobuko Yoshida. Multiparty session types as coherence proofs. In L. Aceto and D. de Frutos-Escrig,
editors, CONCUR, volume 42 of LIPIcs, pages 412–426. Schloss Dagstuhl, 2015.
9. Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, and Luca
Padovani. Global progress for dynamically interleaved multiparty sessions. Mathematical Structures in Computer Science, 26(2):238–302, 2016.
10. Luı́s Cruz-Filipe and Fabrizio Montesi. Choreographies in practice. In Elvira Albert
and Ivan Lanese, editors, FORTE, volume 9688 of LNCS, pages 1–10. Springer,
2016.
11. Luı́s Cruz-Filipe and Fabrizio Montesi. A core model for choreographic programming. 2016. Accepted for publication.
12. Mila Dalla Preda, Maurizio Gabbrielli, Saverio Giallorenzo, Ivan Lanese, and Jacopo Mauro. Dynamic choreographies – safe runtime updates of distributed applications. In T. Holvoet and M. Viroli, editors, COORDINATION, volume 9037 of
LNCS, pages 67–82. Springer, 2015.
13. Frank S. de Boer, Mohammad Mahdi Jaghoori, Cosimo Laneve, and Gianluigi
Zavattaro. Decidability problems for actor systems. Logical Methods in Computer
Science, 10(4), 2014.
14. Romain Demangeon and Kohei Honda. Nested protocols in session types. In
CONCUR, pages 272–286, 2012.
15. Pierre-Malo Deniélou and Nobuko Yoshida. Dynamic multirole session types. In
T. Ball and M. Sagiv, editors, POPL, pages 435–446. ACM, 2011.
16. Maurizio Gabbrielli, Saverio Giallorenzo, and Fabrizio Montesi. Applied choreographies. CoRR, abs/1510.03637, 2015.
17. Kohei Honda, Vasco Vasconcelos, and Makoto Kubo. Language primitives and
type disciplines for structured communication-based programming. In C. Hankin,
editor, ESOP, volume 1381 of LNCS, pages 122–138. Springer, 1998.
18. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty Asynchronous
Session Types. J. ACM, 63(1):9, 2016.

29

19. Ivan Lanese, Claudio Guidi, Fabrizio Montesi, and Gianluigi Zavattaro. Bridging
the gap between interaction- and process-oriented choreographies. In A. Cerone
and S. Gruner, editors, SEFM, pages 323–332. IEEE, 2008.
20. Ivan Lanese, Fabrizio Montesi, and Gianluigi Zavattaro. Amending choreographies.
In Proceedings 9th International Workshop on Automated Specification and Verification of Web Systems, WWV 2013, Florence, Italy, 6th June 2013., pages 34–48,
2013.
21. Tanakorn Leesatapornwongsa, Jeffrey F. Lukman, Shan Lu, and Haryadi S. Gunawi. TaxDC: A taxonomy of non-deterministic concurrency bugs in datacenter
distributed systems. In ASPLOS, pages 517–530. ACM, 2016.
22. Shan Lu, Soyeon Park, Eunsoo Seo, and Yuanyuan Zhou. Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. ACM
SIGARCH Computer Architecture News, 36(1):329–339, 2008.
23. Fabrizio
Montesi.
Choreographic
Programming.
Ph.D.
Thesis,
IT
University
of
Copenhagen,
2013.
http://fabriziomontesi.com/files/choreographic programming.pdf .
24. Fabrizio Montesi and Nobuko Yoshida. Compositional choreographies. In P.R.
D’Argenio and H.C. Melgratti, editors, CONCUR, volume 8052 of LNCS, pages
425–439. Springer, 2013.
25. MPI Forum. MPI: A Message-Passing Interface Standard. High-Performance Computing Center Stuttgart, 2015. Version 3.1.
26. John C. Reynolds. Separation logic: A logic for shared mutable data structures.
In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July
2002, Copenhagen, Denmark, Proceedings, pages 55–74. IEEE Computer Society,
2002.
27. Davide Sangiorgi and David Walker. The π-calculus: a Theory of Mobile Processes.
Cambridge University Press, 2001.
28. Vasco Thudichum Vasconcelos, Simon J. Gay, and António Ravara. Type checking
a multithreaded functional language with session types. Theor. Comput. Sci.,
368(1–2):64–87, 2006.
29. W3C WS-CDL Working Group. Web services choreography description language
version 1.0. http://www.w3.org/TR/2004/WD-ws-cdl-10-20040427/, 2004.
30. Nobuko Yoshida, Pierre-Malo Deniélou, Andi Bejleri, and Raymond Hu. Parameterised multiparty session types. In C.-H. Luke Ong, editor, FOSSACS, volume
6014 of LNCS, pages 128–145. Springer, 2010.

30

A

Detailed definitions and proofs

We report on definitions and proofs that were omitted from the main part of
this paper, as well as some more detailed examples.
A.1

Type checking and type inference

We start with some technical lemmas about typing.
Lemma 1 (Monotonicity). Let Γ and Γ ′ be typing contexts with Γ ⊆ Γ ′ , G1 ,
G′1 and G be connection graphs such that G1 ⊆ G, and C be a choreography. If
Γ ; G1 ⊢ C ⊲ G′1 , then Γ ′ ; G ⊢ C ⊲ G ∪ G′1 .
Proof. Straightforward by induction on the derivation of Γ ; G1 ⊢ C ⊲ G′1 .
Lemma 2 (Sequentiality). Let Γ be a typing context, G1 , G′1 , G2 and G′2 be
connection graphs such that G2 ⊆ G′1 , and C1 , C2 be choreographies. If Γ ; G1 ⊢
C1 ⊲ G′1 and Γ ; G2 ⊢ C2 ⊲ G′2 , then Γ ; G1 ⊢ C1 # C2 ⊲ G′1 ∪ G′2 .
Proof. Straightforward by induction on the derivation of Γ ; G2 ⊢ C2 ⊲ G′2 .
Lemma 3 (Substitution). Let Γ be a typing context, G and G′ be connection
graphs, and C be a choreography. Let p̃ be a set of process names that are free
in C and q̃ be a set of process names that do not occur (free or bound) in C. If
Γ ; G ⊢ C ⊲ G′ , then Γ [p̃/q̃]; G[p̃/q̃] ⊢ C[p̃/q̃] ⊲ G′ [p̃/q̃].
Proof. Straightforward by induction on the derivation of Γ ; G ⊢ C ⊲ G′ , as all
typing rules are valid when substitutions are applied.
We are now ready to start proving Theorem 1. The following lemma takes
care of the base cases, and is required for one of the inductive steps.
Lemma 4. Let Γ be a set of typing judgements, D a set of procedure definitions,
G1 and G′1 connection graphs, and C a choreography that does not start with
0 or a procedure call. Assume that Γ ⊢ D and Γ ; G1 ⊢ C ⊲ G′1 . For every
state σ, there exist Γ ′ , σ ′ , C ′ , G2 and G′2 such that G1 , C, σ →D G2 , C ′ , σ ′ and
Γ ′ ; G2 ⊢ C ′ ⊲ G′2 .
Proof. By case analysis on the last step of the proof of Γ ; G1 ⊢ C ⊲ G′1 . By hypothesis, this proof cannot end with an application of rules ⌊T|End⌉, ⌊T|EndSeq⌉
or ⌊T|Call⌉; we detail all cases for completeness, but the only non-trivial one is
the last.
– ⌊T|Start⌉: then C is p start qT ; C ◦ and by hypothesis
Γ, q : T ; G1 ∪ {p ↔ q} ⊢ C ◦ ⊲ G′1 .
Since G1 , p start qT ; C, σ →D G1 ∪ {p ↔ q}, C ◦ , σ[q 7→ ⊥T ] by rule ⌊C|Start⌉,
taking Γ ′ = Γ, q : T , σ ′ = σ[q 7→ ⊥T ], C ′ = C ◦ , G2 = G1 ∪ {p ↔ q} and
G′2 = G′1 establishes the thesis.
31

G

1
q, f [σ(q)/∗](e[σ(p)/∗])
– ⌊T|Com⌉: then C is p.e -> q.f ; C ◦ and by hypothesis p ←→
′
is a valid expression of type Tq , and Γ ; G1 ⊢ C⊲G1 . Then all the preconditions
of ⌊C|Com⌉ are met, so taking Γ ′ = Γ , σ ′ = σ[q 7→ f [σ(q)/∗](e[σ(p)/∗])],
C ′ = C ◦ , G2 = G1 and G′2 = G′1 establishes the thesis.

G

1
q and Γ ; G1 ⊢ C⊲G′1 .
– ⌊T|Sel⌉: then C is p -> q[l]; C ◦ and by hypothesis p ←→
◦
◦
By ⌊C|Sel⌉, G1 , p -> q[l]; C , σ →D G1 , C , σ, so taking Γ ′ = Γ , σ ′ = σ,
C ′ = C ◦ , G2 = G1 and G′2 = G′1 again establishes the thesis.

G

G

1
1
r,
q, p ←→
– ⌊T|Tell⌉: then C is p : q <-> r; C ◦ and by hypothesis both p ←→
◦
′
and Γ ; G1 ∪ {q ↔ r} ⊢ C ⊲ G1 . Since the preconditions of rule ⌊C|Tell⌉ are
met, by taking Γ ′ = Γ , σ ′ = σ, C ′ = C ◦ , G2 = G1 ∪ {q ↔ r} and G′2 = G′1
establishes the thesis.
– ⌊T|Cond⌉: then C is if p.e then C1 else C2 ; C ◦ and by hypothesis e[σ(p)/∗] is
a valid Boolean expression, Γ ; G1 ⊢ Ci ⊲ G◦i and Γ ; G◦1 ∩ G◦2 ⊢ C ◦ ⊲ G′1 .
Suppose e[σ(p)/∗] = true (the other case is similar). Then G1 , if p.e then C1 else C2 ; C ◦ , σ →D
G1 , C1 # C, σ. Since G◦1 ∩ G◦2 ⊆ G◦1 , Lemma 2 allows us to conclude that
Γ ; G1 ⊢ C1 # C ⊲ G′1 ∪ G◦1 , whence the thesis follows by taking Γ ′ = Γ ,
C ′ = C1 # C, G2 = G1 and G′2 = G′1 ∪ G◦1 .

Proof (Theorem 1). If C D 0, then the first case holds. Assume that C 6D 0;
we show that the second case holds by induction on the proof of Γ ; G1 ⊢ C ⊲
G′1 . By hypothesis, the last rule applied in this proof cannot be ⌊T|End⌉; the
cases where the last rule applied is ⌊T|Start⌉, ⌊T|Com⌉, ⌊T|Sel⌉, ⌊T|Tell⌉ or
⌊T|Cond⌉ follow immediately from Lemma 4, while the case of rule ⌊T|EndSeq⌉
is straightforward from the induction hypothesis.
We focus on the case of rule ⌊T|Call⌉. In this case, C has the form Xhp̃i; C ◦ ,
′
T ) : (G
and we know that Γ ⊢ X(qf
X ⊲ GX ), Γ ⊢ p̃ : T , GX [p̃/q̃] ⊆ G1 and
′
◦
′
Γ ; G1 ∪ (GX [p̃/q̃]) ⊢ C ⊲ G1 . From the hypothesis that Γ ⊢ D we also know
that ΓX ; GX ⊢ CX ⊲ G′X , where CX is the body of X as defined in D. By
Lemma 3, ΓX [p̃/q̃]; GX [p̃/q̃] ⊢ CX [p̃/q̃] ⊲ G′X [p̃/q̃], whence by Lemma 1 also
Γ ; G1 ⊢ CX [p̃/q̃] ⊲ G′X [p̃/q̃] ∪ G1 . By applying rule ⌊C|Unfold⌉, we conclude that
Xhp̃i; C ◦ D CX [p̃/q̃] # C ◦ , and Lemma 2 allows us to conclude that Γ ; G1 ⊢
CX [p̃/q̃] # C ◦ ⊲ G′1 . Since procedure calls are guarded, CX does not begin with a
procedure call, and Lemma 4 establishes the thesis.
Proof (Theorem 2). The proof of this result proceeds in several stages. We first
observe that deciding whether Γ ; G ⊢ C ⊲ G′ is completely mechanical, as the
typing rules are deterministic. Furthermore, those rules can also be used to
construct G′ from G and C; therefore, the key step of this proof is showing, given
Γ and hD, Ci, how to find a “canonical typing” for the recursive definitions,
the set ΓD , such that ΓD ⊢ D and Γ, ΓD ; GC ⊢ C ⊲ G′ (with G′ inferred) iff
Γ, Γ ′ ; GC ⊢ C ⊲ G′′ for some Γ ′ and G′′ . More precisely, we need to find graphs
GX and G′X for each procedure X defined in D.
Our proof proceeds in three steps. First, for each X we compute an underapproximation G◦X of the output graph G′X , containing all the relevant connections
that executing X can add. Using this, we are able to compute the input graph
32

GX and the output graph G′X = GX ∪G◦X . Both these steps are achieved by computing a minimal fixpoint of a monotonic operator in the set of all graphs whose
vertices are the parameters of X. Finally, we argue that the typing X : GX ⊲ GX
is minimal, and therefore the set ΓD of all such typings fulfills the property we
require.
Throughout the remainder of this proof, we assume D = {Xi (qei ) = Ci | i =
1, . . . , n}.
1. In order to compute G◦Xi , we define an auxiliary function fwd with intended
i
meaning as follows: fwdG̃
Cj (G) computes the communication graph obtained
from G after one execution of the body of Xj , assuming that Xi (qei ) : ∅ ⊲ Gi
for all i and ignoring newly created processes. We use a conditional union
operator ⊎ where G ⊎ {e} denotes G ∪ {e} if e is an edge connecting two
vertices in G, and G otherwise. The function fwd is defined as follows.
i
fwdG̃
0 (G) = G

G̃i
i
fwdG̃
0;C (G) = fwdC (G)
i
i
fwdG̃
(G) = fwdG̃
C (G)
p.e -> q.f ;C

i
i
fwdG̃
(G) = fwdG̃
C (G)
p -> q[l];C
i
i
fwdG̃
(G) = fwdG̃
C (G)
p start qT ;C
i
i
fwdG̃
(G) = fwdG̃
C (G ⊎ {q ↔ r})
p:q <-> r;C

G̃i
G̃i
G̃i
i
fwdG̃
if p.e then C1 else C2 ;C (G) = fwdC (fwdC1 (G) ∩ fwdC2 (G))
i
i
ei
fwdG̃
(G) = fwdG̃
C (G ⊎ Gi [p̃/q ])
Xi hp̃i;C

Using fwd, we define an operator Tfwd over the set G of tuples of graphs over
fi | Gi is a graph over qei }. Observe that G
the parameters of Xi , i.e. G = {G
is a complete lattice wrt componentwise inclusion.
G̃i
fi ) = fwd^
Tfwd (G
Ci (Gi )

This operator is monotonic, since fwd only adds edges to its argument, and
thus has a least fixpoint that can be computed by iterating Tfwd from the
tuple of empty graphs over the right sets of vertices. Furthermore, since G is
finite (each graph has a finite number of vertices) this fixpoint corresponds
to a finite iterate, and can thus be computed in finite time. We denote this
◦ .
g
fixpoint by G
Xi
2. The construction of the input graphs GXi follows the same idea: we go
through the Ci s noting the edges that are required for all communications
to be able to take place. It is however slightly more complicated, because
we have to keep track of edges that the choreography adds to the graph; we
therefore need a function bck that manipulates two graphs instead of one.
33

i
More precisely, bckG̃
C (G, G) returns the graph extending G that is needed for
correctly executing C (ignoring newly created processes); the first argument
keeps track of the edges that need to be added to G, and the second argument
keeps track of edges added by executing C. This function uses the graphs
G◦Xi computed earlier, which explains why it has to be defined afterwards.
We use the same notational conventions as above, and let fstha, bi = a and
sndha, bi = b. The definition of bck is given in Figure 16; it is not the simplest

G̃

bck0 i (Ga , Gb ) = hGa , Gb i
G̃

˜
G

i
bck0;C
(Ga , Gb ) = bckC i (Ga , Gb )
(
G̃
bckC i (Ga , Gb )
G̃
bckp.ei -> q.f ;C (Ga , Gb ) =
G̃i
bckC (Ga ⊎ {p ↔ q}, Gb ⊎ {p ↔ q})
(
G̃
bckC i (Ga , Gb )
G̃i
bckp ->
(Ga , Gb ) =
G̃i
q[l];C
bckC (Ga ⊎ {p ↔ q}, Gb ⊎ {p ↔ q})
G̃i
(Ga , Gb )
p start qT ;C

bck

G̃

if p ↔ q ∈ Gb
otherwise
if p ↔ q ∈ Gb
otherwise

˜
G

= bckC i (Ga , Gb )


˜
G

bckC i (Ga , Gb ⊎ {q ↔ r})



˜
G

˜
bckC i (Ga ⊎ {p ↔ q}, Gb ⊎ {p ↔ q, q ↔ r})
G
bckp:qi <-> r;C (Ga , Gb ) =
bckG˜i (Ga ⊎ {p ↔ r}, Gb ⊎ {p ↔ r, q ↔ r})


C


˜
G
bckC i (Ga ⊎ {p ↔ q, p ↔ r}, Gb ⊎ {p ↔ q, p ↔ r, q ↔ r})

i
bckif p.e
then C

(Ga , Gb )
1 else C2 ;C
˜
G
i
bckX hp̃i;C (Ga , Gb )
i

˜
G

G̃

G̃

if p ↔ q, p ↔ r ∈ Gb
if p ↔ q 6∈ Gb , p ↔ r ∈ Gb
if p ↔ q ∈ Gb , p ↔ r 6∈ Gb
if p ↔ q, p ↔ r 6∈ Gb

˜
G

G̃

= bckC i (fst(bckC i (Ga , Gb )) ∪ fst(bckC i (Ga , Gb )), snd(bckC i (Ga , Gb )) ∩ snd(bckC i (Ga , Gb )))
1

2

1

˜
G
ei
= bckC i (Ga ⊎ (Gi [p̃/qei ] \ Gb ), Gb ⊎ Gi [p̃/qei ] ⊎ G◦
i [p̃/q ])

Fig. 16. Definition of bck (case 2 in the proof of Theorem 2).
possible, but the formulation given is sufficient for our purposes.
Again we define a monotonic operator over the same G as above.
G̃i
fi ) = fst(bck^
Tbck (G
Ci (Gi , Gi ))

We do not need to recompute G◦i , since these graphs contain all edges that
can possibly be added by executing Ci . The least fixpoint of Tbck can again
g
be computed by finitely iterating this operator, and it is precisely G
Xi . We
′
◦
then define GXi = GXi ∪ GXi .
3. We now show that ΓD = {Xi (qei ) : GXi ⊲ G′Xi } is a minimal typing of D,
in the sense explained earlier. Observe that it is possible that ΓD 6⊢ D, in
particular if the Xi are ill-formed choreographies.
Suppose that Γ, Γ ′ ; GC ⊢ C⊲G for some Γ ′ and G. We argue that Γ, ΓD ; GC ⊢
C ⊲ G′ , where G′ is inferred from the typing rules. For each procedure
′
Xi (qei ) = Ci , there must be a unique typing Xi (qei ) : G∗Xi ⊲ G∗∗
Xi in Γ . By
◦
∗∗
a simple inductive argument one can show that GXi ⊆ G (since ∅ ⊆ G∗∗
Xi
∗
and Tfwd preserves inclusion in G∗∗
Xi ). Similarly, one shows that GXi ⊆ GXi
34

2

∗
′
and that G∗∗
Xi \ GXi ⊆ GXi \ GXi . As a consequence, the typing derivation
′
for Γ, Γ ; GC ⊢ C ⊲ G can be used for Γ, ΓD ; GC ⊢ C ⊲ G′ , as all applications
of rule ⌊T|Call⌉ are guaranteed to be valid (their preconditions hold) and
to produce the same results (they change the communication graph in the
same way).

A consequence of this result is that we can obtain a type inference algorithm
(Theorem 3), as we only need to “guess” types for the processes in the choreography. As a corollary of the proof, we can also infer the types for parameters of
procedural definitions and freshly created processes.
Proof (Theorem 3). Construct Γ by going through C and adding p : Tp every
time there is an action that depends on p’s type (i.e. p is a sender or receiver in a
communication, or an argument of a procedure call). If Γ contains two different
types for any process, then output NO, else output Γ . This algorithm will not
necessarily assign a type to all processes in C, in case C contains processes whose
memory is never accessed.
Proof (Theorem 4). Inferring the types of freshly created processes is analogous
to the previous proof.
As for parameters of procedure definitions, we omit the details of the proof,
as it repeats ideas previously used. Define an operator TT over tuples of typing
contexts (one for each Xi defined in D) that generates a typing context for each
Xi in the same way as in the previous proof. If any contradictions are found,
then fail. Iterate TT until either failure occurs (in which case the Xi s are not
properly defined) or a fixpoint is reached. Finally, assign a random type (e.g. N)
to each process variable that has not received a type during this procedure. The
algorithm readily extends to infer the types of processes created inside procedure
definitions.
A.2

EndPoint Projection

Merging. The full definition of merging is given in Figure 17.
Projections of procedure definitions. When projecting procedure definitions, we
simply kept all arguments, and relied on typing to guarantee that no process will
ever attempt to communicate with another process it does not know. However,
it is “cleaner” to refine the definition of projection so that such parameters are
not even formally used.
This is technically not challenging, as we can use typing information to decide which parameters should be kept in each projection. In other words, when
T ) = C]], the projected procedure X will only contain as arcomputing [[X(qf
i
G

X
qj , where GX is given by typing. (This
guments those qj such that qi ←→
definition is non-deterministic, but it can be made deterministic by using the
minimal graph GX computed by the type inference algorithm.) A simple annotation can then ensure that projected procedure calls only keep the arguments

35


= p?f ; B ⊔ B ′




(q!!r; B) ⊔ q!!r; B ′ = q!!r; B ⊔ B ′
(q?r; B) ⊔ q?r; B ′ = q?r; B ⊔ B ′




(q ⊕ l; B) ⊔ q ⊕ l; B ′ = q ⊕ l; B ⊔ B ′
(Xhp̃i; B) ⊔ Xhp̃i; B ′ = Xhp̃i; B ⊔ B ′



(start q ⊲ B2 ; B1 ) ⊔ start q ⊲ B2′ ; B1′ = start q ⊲ B2 ⊔ B2′ ; B1 ⊔ B1′

B1 ⊔ B2 = B1′ ⊔ B2′
if B1  B1′ and B2  B2′
(0; B) ⊔ B ′ = B ⊔ B ′



(if e then B1 else B2 ) ; B ⊔ if e then B1′ else B2′ ; B ′ = if e then (B1 ⊔ B1′ ) else (B2 ⊔ B2′ ) ; B ⊔ B ′



(p&{li : Bi }i∈J ; B) ⊔ p&{li : Bi′ }i∈K ; B ′ = p& {li : (Bi ⊔ Bi′ )}i∈J ∩K ∪ {li : Bi }i∈J \K ∪ {li : Bi′ }i∈K\J ; B ⊔ B ′
(q!e; B) ⊔

q!e; B ′



= q!e; B ⊔ B ′



(p?f ; B) ⊔

p?f ; B ′



Fig. 17. Merging operator in PP.

in the corresponding positions, and typing guarantees that all those arguments
are known at runtime by the process invoking the recursive call.
An implementation of Quicksort showcasing this reasoning was previously
published in [10].
EPP. We sketch the proof of the EPP Theorem.
Proof (Theorem 5 (sketch)). The structure of the proof is standard, from [23],
so we only show the most interesting differing details. In particular, we need to
be careful about how we deal with connections, which is a new key ingredient
in PC wrt to previous work. We demonstrate this point for the direction of
(Completeness); the direction for (Soundness) is proven similarly. The proof
proceeds by induction on the derivation of G, C, σ →D G′′ , C ′ , σ ′ . The interesting
cases are reported below.
– ⌊C|Tell⌉: From the definition of EPP we get:
[[p : q <-> r; C ◦ , σ]] 
p ⊲σ(p) q!!r; [[C ◦ ]]p | q ⊲σ(q) p?r; [[C ◦ ]]q | r ⊲σ(r) p?q; [[C ◦ ]]r | N
By ⌊P|Tell⌉ we get:
[[p : q <-> r; C ◦ , σ]] →
p ⊲σ′ (p) [[C ◦ ]]p | q ⊲σ′ (q) [[C ◦ ]]q | r ⊲σ′ (r) [[C ◦ ]]r | N
which proves the thesis, since we can assume that the projection of C ′ remains unchanged for the other processes (N stays the same).
– ⌊C|Start⌉: This is the most interesting case. From the definition of EPP we
get:
[[p start qT ; C ◦ , σ]]  p ⊲σ(p) start qT ⊲ [[C ◦ ]]q ; [[C ◦ ]]p | N
36

From the semantics of PP we get:
[[p start qT ; C ◦ , σ]] → p ⊲σ′ (p) ([[C ◦ ]]p )[q′ /q] | q′ ⊲⊥T [[C ◦ ]]q′ | N
The Barendregt convention implies C  (p start qT ; C ◦ )[q′ /q]. We now have
to prove that:
[[C ◦ [q′ /q], σ]]  p ⊲σ′ (p) ([[C ◦ ]]p )[q′ /q] | q′ ⊲⊥T [[C ◦ ]]q′ | N
We observe that this is true only if process q does not occur free in N , i.e.,
q appear in N only inside the scope of a binder. The latter must be of the
form r?q; B. This is guaranteed by the fact that C is well-typed, since the
typing rules prevent other processes in N to communicate with q without
being first introduced.
⊓
⊔
Choreography Amendment. We now define precisely an amendment function that
makes every choreography projectable. As mentioned earlier, we follow ideas previously used in other choreography models [20,11]. Observe that, by definition,
the only choreography construct that can lead to unprojectability is the conditional.
Definition 4 (Amendment). Given a choreography C, the transformation
Amend(C) repeatedly applies the following procedure until it is no longer possible, starting from the inner-most subterms in C. For each conditional subterm
if p.e then C1 else C2 in C, let r̃ ⊆ (pn(C1 ) ∪ pn(C2 )) be such that [[C1 ]]r ⊔ [[C2 ]]r is
undefined for all r ∈ r̃; then if p <= q then C1 else C2 in C is replaced with:
if p.e then p -> r1 [l]; · · · ; p -> rn [l]; C1
else p -> r1 [r]; · · · ; p -> rn [r]; C2
By the definitions of Amend and EPP and the semantics of PC, we get the
following properties, where →∗ is the transitive closure of →.
Theorem 9 (Amendment). Let C be a choreography. Then:
(Completeness) Amend(C) is defined;
(Projectability) for all σ, [[Amend(C), σ]] is defined;
(Correspondence) for all G, σ and D:
– if G, C, σ →D G′ , C ′ , σ, then G, Amend(C), σ →∗D G′ , Amend(C ′ ), σ ′ ;
– if G, Amend(C), σ →D G′ , C ′ , σ ′ , then there exist C ′′ and σ ′′ such that
G, C, σ →D G′ , C ′′ , σ ′′ and G′ , C ′ , σ ′ →∗D G′ , C ′′ , σ ′′ .
Proof (Theorem 9). (Completeness) and (Projectability) are immediate by definition of Amend. For (Correspondence), the proof is by analysis of the possible
transitions. The only interesting cases occur when the transition consumes a
conditional. In the case G, C, σ → G′ , C ′ , σ, then Amend(C) also has to consume
the label selections introduced by amendment in the branch taken in order to
reach Amend(C ′ ). Conversely, if G, Amend(C), σ makes a transition that consumes a conditional, then C ′ needs to consume the label selections introduced
by amendment in order to match the corresponding move by C.
37

G

p→q

e[σ(p)/∗] ↓ v

⌊C|Com-S⌉

x

G, p.e -> •q ; C, σ →D G, C[v/x], σ
G

q→p

f [σ(q)/∗](v) ↓ w

⌊C|Com-R⌉

v

G, •p -> q.f ; C, σ →D G, C, σ[q 7→ w]
G

p→q

⌊C|Sel-S⌉

x

G, p -> •q [l]; C, σ →D G, C[l/x], σ
G

q→p

⌊C|Sel-R⌉

l

G, •p -> q[l]; C, σ →D G, C, σ
G

G

p→q

p→r

x,y

⌊C|Tell-S⌉

G, p : •q <-> •r ; C, σ →D G, C[q/x, r/y], σ
G

q→p

⌊C|Tell-R⌉

r

G, •p .r -> q; C, σ →D G ∪ {q → r}, C, σ

Fig. 18. Asynchronous PC, Semantics of New Runtime Terms.
This result also holds if we replace D by Amend(D) in the relevant places.
The first choreography in Remark 2, which is unprojectable, can be amended
to the projectable choreography presented at the end of the same remark.
A.3

Asynchrony

We detail the whole sets of rules for the semantics of aPC (Figure 18) and its
type system (Figure 19), as well as for the semantics of aPP (Figure 20). The
full definition of EPP is given in Figures 21 and 22.
The proofs of the relationships between PC/PP and their asynchronous counterparts are mechanical.
Proof (Theorem 6). Straightforward by case analysis on the possible transitions
of C.
Proof (Theorem 7). Straightforward by case analysis on the possible transitions
of N .
A.4

Procedures with holes

We illustrate the use of holes to define a general-purpose iterator, procedure
Iter below. Using Iter, we define a procedure Reverse for reversing the list of
a process q. We omit the straightforward procedures for decrementing a counter
and popping a list.
38

G

p→q

Γ ⊢ p : Tp

Γ ⊕ (x : T ); G ⊢ C ⊲ G′

∗ : T p ⊢T e : T
x

Γ ; G ⊢ p.e -> •q ; C ⊲ G′
G

q→p

Γ ⊢ q : Tq

∗ : T q ⊢T f : T → T q

⌊T|Com-S⌉

Γ ⊕ (x : T ); G ⊢ C ⊲ G′

x

Γ ; G ⊢ •p -> q.f ; C ⊲ G′
G

q→p

Γ ⊢ q : Tq

⊢T v : T

⌊T|Com-RV⌉

Γ ; G ⊢ C ⊲ G′

∗ : T q ⊢T f : T → T q
v

Γ ; G ⊢ •p -> q.f ; C ⊲ G′
G

Γ ⊕ (x = l); G ⊢ C ⊲ G′

p→q

⌊T|Sel-S⌉

x

Γ ; G ⊢ p -> •q [l]; C ⊲ G′
G

q→p

Γ ⊕ (x = l); G ⊢ C ⊲ G′
x

Γ ; G ⊢ •p -> q[l]; C ⊲ G′
G

G

p→q

p→r

G

⌊T|Sel-RV⌉

q→p

l

Γ ⊕ (x = q) ⊕ (y = r) ⊢ C ⊲ G′
x,y

G

Γ ; G ∪ {q → r} ⊢ C ⊲ G′
r

Γ ; G ⊢ •p .r -> q; C ⊲ G′
G

q→p

Γ ; G ⊢ C ⊲ G′

x

⌊T|Tell-S⌉

⌊T|Tell-RV⌉

Γ ⊕ (x = r); G ∪ {q → r} ⊢ C ⊲ G′
Γ ; G ⊢ •p .r -> q; C ⊲ G′

⌊T|Sel-RT⌉

Γ ; G ⊢ •p -> q[l]; C ⊲ G′

Γ ; G ⊢ p : •q <-> •r ; C ⊲ G′
q→p

⌊T|Com-RT⌉

⌊T|Tell-RT⌉

Fig. 19. Asynchronous PC, Typing Rules (New Runtime Terms).

Iter (p ,q , r ) = if p . is_zero
then p -> q , r [ stop ]
else dec <p >; p -> q , r [ cont ]; h ; Iter <p ,q ,r >
Reverse ( q ) =
q starts p , r ; q : p < - > r ;
q . size -> p ; q . empty -> r ;
Iter <p ,q ,r > with h 7→ q . top -> r . append ; pop <q >;
r .* -> q

39

ρ′q = ρq · hp, e[v/∗]i
ρ

ρ

⌊P|Com-S⌉

ρ′

ρ

p ⊲vp q!e; Bp | q ⊲wq Bq →B p ⊲vp Bp | q ⊲wq Bq
ρq  hp, vi · ρ′q
q

ρ
⊲wq

⌊P|Com-R⌉

ρ′

p?f ; B →B q ⊲uq B

ρ′q = ρq · hp, ri
ρ

u = (f [w/∗])(v)

ρ′r = ρr · hp, qi
ρ′

ρ

ρ

⌊P|Tell-S⌉

ρ′

p ⊲vp q!!r; Bp | q ⊲wq Bq | r ⊲ρz r Br →B p ⊲vp Bp | q ⊲wq Bq | r ⊲z r Br
ρq  hp, ri · ρ′q

⌊P|Tell-R⌉

ρ′

ρ

q ⊲wq p?r; B →B q ⊲wq B
ρ′q = ρq · hp, li
ρ

ρ

ρ′

ρ

⌊P|Sel-S⌉

p ⊲vp q ⊕ l; B | q ⊲wq Bq →B p ⊲vp B | q ⊲wq Bq
ρq  hp, lj i · ρ′q

j∈I

⌊P|Sel-R⌉

ρ′

ρ

q ⊲wq p&{li : Bi }i∈I →B q ⊲wq Bj

Fig. 20. Asynchronous Procedural Processes, Semantics (New Rules).
(

(
v̂
q!e; [[C]]r if r = p
p?f ; [[C]]r
[[p.e -> •q ; C]]r =
[[•p -> q.f ; C]]r =
[[C]]r
otherwise
[[C]]r
(
(
l̂
x
p&{l : [[C]]r }
q ⊕ l if r = p
[[•p -> q[l]; C]]r =
[[p -> •q [l]; C]]r =
[[C]]r
[[C]]r otherwise
(
(
x,y
p̂
q!!r; [[C]]s if s = p
p?r; [[C]]s
[[p : •q <-> •r ; C]]s =
[[•p .r -> q; C]]s =
[[C]]s
otherwise
[[C]]s
x

if r = q
otherwise
if r = q
otherwise
if s = q
otherwise

Fig. 21. Asynchronous PC, Behaviour Projection (New Rules).

v

(|•p -> q.f ; C|)r =

(

hp, vi · (|C|)r
(|C|)r
r

if r = q
otherwise
(

(|•p .r -> q; C|)s =

l

(|•p -> q[l]; C|)r =
hp, ri · (|C|)s
[[C]]s

(|if p <= q then C1 else C2 ; C|)r = (|C1 |)r · (|C|)r

(

if r = q
otherwise

if s = q
otherwise
(|η; C|)r = (|I; C|)r = (|C|)r

Fig. 22. Asynchronous PC, State Projection.

40

hp, li · (|C|)r
[[C]]r

