Classical Higher-Order Processes
(Technical Report)
FABRIZIO MONTESI, University of Southern Denmark

arXiv:1802.02917v1 [cs.LO] 8 Feb 2018

Classical Processes (CP) is a calculus where the proof theory of classical linear logic types communicating processes with mobile
channels, à la π -calculus. Its construction builds on a recent propositions as types correspondence between session types and
propositions in linear logic. Desirable properties such as type preservation under reductions and progress come for free from the
metatheory of linear logic.
We contribute to this research line by extending CP with code mobility. We generalise classical linear logic to capture higher-order
(linear) reasoning on proofs, which yields a logical reconstruction of (a variant of) the Higher-Order π -calculus (HOπ ). The resulting
calculus is called Classical Higher-Order Processes (CHOP). We explore the metatheory of CHOP, proving that its semantics enjoys
type preservation and progress (terms do not get stuck). We also illustrate the expressivity of CHOP through examples, derivable
syntax sugar, and an extension to multiparty sessions. Lastly, we define a translation from CHOP to CP, which encodes mobility of
process code into reference passing.
CCS Concepts: •Theory of computation → Distributed computing models; Process calculi; Linear logic; •Software and its
engineering → Concurrent programming structures;
Additional Key Words and Phrases: Higher-order Processes, Session Types, Linear Logic, Propositions as Types

1

INTRODUCTION

Session types (Honda et al. 1998) define protocols that discipline communications among concurrent processes, typically
given in terms of (variants of) the π -calculus (Milner et al. 1992). In their seminal paper, Caires and Pfenning (2010)
established a Curry-Howard correspondence between the type theory of sessions and intuitionistic linear logic, where
processes correspond to proofs, session types to propositions, and communication to cut elimination. Important
properties that are usually proven with additional machinery on top of session types, like progress, come for free from
the properties of linear logic, like cut elimination. Wadler (2014) revisited the correspondence for Classical Linear Logic
(CLL), developing the calculus of Classical Processes (CP). CP enjoys a stricter correspondence with linear logic, and
branched off a new line of development wrt the π -calculus: CP foregoes the standard semantics of π -calculus, and
instead adopts a semantics that is dictacted by standard proof transformations found in linear logic. Therefore, CP
serves two important purposes: it shows how to use linear logic “directly” as a solid foundation for protocol-driven
concurrent programming; and it is a convenient model to explore extensions of linear logic that are interesting in the
setting of process models.
In this article, we extend this research line to capture code mobility—the capability to communicate processes—by
logically reconstructing the generalisation of the π -calculus into the Higher-Order π -calculus (HOπ ) (Sangiorgi 1993).
Mobile code is widespread. For example, it is a cornerstone of mobile application stores and cloud computing. Disciplined
programming in these settings is key, since a host may have to run arbitrary code received from a third party, and such
code does might then interact with the host itself and its environment. This motivates the search for solid foundations
for disciplining the programming of mobile code, as we may hope to do with linear logic.
1

Outline of development and contributions. We develop the calculus of Classical Higher-Order Processes (CHOP), a
strict generalisation of CP that captures process mobility (CP is a fragment of CHOP). CHOP extends linear logic to
higher-order reasoning, by allowing proofs to have “holes”: a proof may just assume a sequent to be provable and use
it as a premise. Actual proofs that resolve these assumptions can then be provided separately, using a higher-order
version of the cut rule. Providing a proof and assuming provability are respectively typed by two new kinds of types,
[Γ] and hΓi, where Γ is a typing context. The rules that we introduce for our new ingredients type the key primitives
that elevate CP to a higher-order process calculus: send a process, receive a process, store a process in a variable, and
run the process stored in a variable.
Differently from previous higher-order process calculi, CHOP treats process variables linearly (following the intuition
that it is a higher-order linear logic): a process sent over a channel is guaranteed to be eventually used exactly once—the
receiver may delegate this responsibility further on to another process. Higher-order types can be composed using the
standard connectives of linear logic, so that we can apply the usual expressivity of linear logic propositions to this new
setting—e.g., multiple assumptions hΓi ⊗ hΓ 0 i or explicit weakening ?hΓi.
Our higher-order cuts (called chops) support type-preserving proof transformations that yield a semantics of
communication and explicit substitutions (as originally developed by Abadi et al. (1991) for the λ-calculus) for higherorder processes. Our semantics suggests how the substitutions that should be performed at the receiver as a result of
code mobility can be implemented efficiently. We show that the existing semantics for link terms in CP—which bridge
two channels and enable behavioural polymorphism—becomes unsound in the higher-order setting, and then formulate
a sound semantics by generalising η-expansion in CP to higher-order I/O. That η-expansion works as expected for our
new higher-order types also provides evidence of the correct formulation of our new rules.
We investigate the metatheory of CHOP, showing that our semantics preserves types and that processes enjoy
progress (communications between communicating processes never get stuck).
The design of CHOP is intentionally minimalistic, since it is intended as a foundational calculus. We illustrate more
sophisticated features as extensions that build on top of the basic theory of CHOP. Specifically, we discuss how to
implement higher-order I/O primitives with continuations and multiparty sessions.
We conclude our development by presenting a translation of CHOP into CP, which preserves types (up to encoding
of higher-order types into channel types of CP). The translation works by using channel mobility to simulate code
mobility, recalling that presented by Sangiorgi (1993).

Structure of the paper. Section 2 provides an introduction to (the multiplicative fragment of) CP and an overview
of the key insights behind its generalisation to CHOP. Section 3 presents CHOP and a running example that covers
its syntax, typing, and semantics. In section 4, we study the metatheory of CHOP. In section 5, we illustrate how to
extend CHOP with syntax sugar and the support for multiparty sessions. The translation of CHOP to CP is presented in
section 6. We discuss related work in section 7 and present conclusions in section 8.

Differences from previously published material. A short conference paper describing preliminary work in progress
on the development of CHOP has been previously published (Montesi 2017). That paper presented only a draft of
the typing rules for process mobility, which have since been changed (although they are similar, the old ones do not
support the properties that we present here). Aside from motivation and general idea, the present report is thus almost
entirely new. Specifically, it includes the following improvements: a more detailed presentation in sections 1 and 8; full
2

definitions (in section 3); all examples are new (e.g., in section 3); section 4, which reports on properties and proofs, is
new; section 5, covering extensions, is new; section 6, the translation from CHOP to CP, is new.

2

OVERVIEW: FROM CP TO CHOP

We give an overview of some basic notions of CP that we are going to use in this work, and of the key insights behind
our technical development.

2.1

Multiplicative CP

First, we recall the multiplicative fragment of the calculus of Classical Processes (CP), according to its latest version by
Carbone et al. (2016).
Processes and Typing. In CP, processes communicate by using channels, which represent endpoints of sessions. Let
x, y, . . . range over channel names (also called channels, for brevity). Then, the syntax of processes (P, Q, R, . . .) is the
following.
P, Q, R ::=

x[y].(P | Q)

output a channel

x(y).P

input a channel

x[]

close

x().P

wait

(νx Ay) (P | Q)

parallel composition

An output term x[y].(P | Q) sends a fresh name y over x, and then proceeds as the parallel composition of P and
Q. Dually, an input term x(y).P receives a name y on x and then proceeds as P. Names that are sent or received are
bound (y in our syntax for output and input). Term x[] closes endpoint x, and term x().P waits for the closing of x and
then proceeds as P. In general, in CP, square brackets indicate output and round brackets indicate input. The parallel
composition term (νx Ay) (P | Q) connects the endpoints x at process P and y at process Q to form a session, enabling
the two processes to communicate. The names x and y are bound. The type A describes the behaviour that the processes
will follow when communicating.
The types (A, B, C, . . .) of multiplicative CP are exactly the propositions of multiplicative classical linear logic (Girard
1987). A type abstracts how a channel is used by a process. We recall them below, together with a description of their
interpretation as behavioural types for channels in CP.
A, B, C ::=

A⊗B
AOB

send A, proceed as B
receive A, proceed as B

1

unit for ⊗

⊥

unit for O

The notion of duality of linear logic is used in CP to establish whether two types are compatible. Formally, we write A⊥
for the dual of type A. Duality is defined inductively as follows.
(A ⊗ B)⊥

=

(A O B)⊥

=

1⊥

=

⊥

⊥⊥

=

1

3

A⊥ O B ⊥
A⊥ ⊗ B ⊥

` P :: Γ, y : A ` Q :: ∆, x : B
⊗
` x[y].(P | Q) :: Γ, ∆, x : A ⊗ B

` x[] :: x : 1

` P :: Γ, x : A

` P :: Γ
⊥
` x().P :: Γ, x : ⊥

1

` P :: Γ, y : A, x : B
O
` x(y).P :: Γ, x : A O B
`

(νx Ay) (P

` Q :: ∆, y : A⊥
Cut

| Q) :: Γ, ∆

Fig. 1. Multiplicative CP, Typing Rules.

A process may use arbitrarily many channels. Therefore, the types of the channels used by a process are collected in
a typing environment (Γ, ∆, Σ, . . .). Formally, a typing environment associates channel names to types, e.g., Γ = x 1 :
A1 , . . . , x n : An for some natural number n, where all x i in Γ are distinct. Order in environments is ignored (we silently
allow for exchange). Environments can be combined when they do not share names, written Γ, ∆.
Using types (and environments), we can type programs in multiplicative CP (processes) by using the typing rules
given in fig. 1.1 In the rules, a typing judgement ` P :: x 1 : A1 , . . . , x n : An reads “process P implements behaviour Ai
on each channel x i ”. The rules are exactly those from multiplicative classical linear logic, and enforce linear usage of
names. Rule ⊗ types an output x[y].(P | Q) as A ⊗ B by checking that the continuation P will implement behaviour
A on y and behaviour B on x. Dually, rule O types an input x(y).P by checking that the continuation P implements
behaviour A on y and behaviour B on x. Rules 1 and ⊥ are straightforward. Rule Cut types a parallel composition

(νx Ay) (P | Q) by using duality of types. Specifically, we check that the processes P and Q implement dual behaviour
on the respective channels x and y.
Semantics and Properties. The culmination of CP is the semantics that we obtain from its definition. Specifically, we
can reuse the metatheory of cut elimination for linear logic in order to get a semantics for processes with nontrivial
properties. Consider the following example of an application of Cut.
` P :: Γ, x 0 : A ` Q :: Γ 0, x : B
⊗
` x[x 0 ].(P | Q) :: Γ, Γ 0, x : A ⊗ B

` R :: ∆, y 0 : A⊥ , y : B ⊥
` y(y 0 ).R :: ∆, y : A⊥ O B ⊥

` (νx A ⊗B y) (x[x 0 ].(P | Q) | y(y 0 ).R) :: Γ, Γ 0, ∆

O

Cut

The definitions of P, Q, R, Γ, ∆, A, and B are irrelevant for this example: the following reasoning holds in general,
assuming that the premises ` P :: Γ, x 0 : A, ` Q :: Γ 0, x : B, and ` R :: ∆, y 0 : A⊥ , y : B ⊥ are derivable. The reader familiar
with linear logic may have recognised that this example is a case of the proof of cut elimination. In general, cuts can
always be eliminated from linear logic proofs, by following an inductive proof-rewriting procedure. CP inherits this
property. Here, we can rewrite the proof above to use cuts on smaller types, eliminating the ⊗ connective.
` Q :: Γ 0, x : B
` P ::

Γ, x 0

:A

`

` R :: ∆, y 0 : A⊥ , y : B ⊥

(νx B y) (Q

| R) :: Γ 0, ∆, y 0 : A⊥

` (νx 0Ay 0 ) (P | (νx B y) (Q | R) ) :: Γ, Γ 0, ∆

Cut
Cut

This is called a cut reduction. Observe what happened to the initial process. We have rewritten it as follows.
(νx A ⊗B y) (x[x 0 ].(P | Q) | y(y 0 ).R) −→ (νx 0Ay 0 ) (P | (νx B y) (Q | R))
original presentation of CP has an equivalent, but slightly different, syntax for typing judgements: P ` Γ instead of our ` P :: Γ . Our syntax is
convenient for the technical development that comes in the next sections, since we will add a separate higher-order context (Θ) on the left: Θ ` P :: Γ .

1 The

4

This reduction rule executes a communication between two compatible processes composed in parallel. The remarkable aspect of CP is that we obtained the reduction from something that we already know from linear logic, which is
the proof transformation that we discussed: we just need to observe what happens to the processes. Furthermore, it is
evident from the construction of the transformation that it preserves types. All rules for the operational semantics of
CP are built by following this method. We report here the principal reductions for multiplicative CP, and the rules for
allowing reductions inside of cuts.
(νx A ⊗B y) (x[x 0 ].(P | Q) | y(y 0 ).R) −→ (νx 0Ay 0 ) (P | (νx B y) (Q | R))
(νx 1y) (x[] | y().P) −→ P
(νx Ay) (P1 | Q) −→ (νx Ay) (P2 | Q)
(νx Ay) (P

| Q 1 ) −→

(νx Ay) (P

| Q2)

if P1 −→ P2
if Q 1 −→ Q 2

The way in which the semantics of CP is defined gives us two results on a silver platter. First, all reductions in
CP preserve typing (type preservation), because cut elimination preserves types. Second, all sessions are eventually
completely executed (progress), because all cuts can be eliminated from proofs.
2.2

From CP to CHOP

We attempt at applying the same method used for the construction of CP to extend it to process mobility with higherorder primitives. More specifically, we need to find out how we can extend the proof theory of CP with rules that (i)
type new process terms that capture the feature of process mobility, and (ii) enable proof transformations that yield
their expected semantics.
Processes. What kind of process terms enable process mobility? For this, we can get direct inspiration from HOπ . We
need three basic terms.
• A term for sending process code over a channel.
• A term for receiving process code over a channel and storing it in a process variable.
• A term for running the process code stored in a variable.
We thus extend the syntax of multiplicative CP as follows, where p, q, r, . . . range over process variables.
P, Q, R ::=

...
x[(ρ)P]

higher-order output

x(p).Q

higher-order input

phρi

run

The higher-order output term x[(ρ)P] sends the abstraction (ρ)P over channel x. An abstraction is a parameterised
process term, enabling the reuse of process code in different contexts. The concept of abstraction is standard in the
literature of HOπ (Sangiorgi and Walker 2001); here, we apply a slight twist and use named formal parameters ρ rather
than just a parameter list, to make the invocation of abstractions not dependent on the order in which actual parameters
are passed. This plays well with the typing contexts of linear logic, used for typing process terms in CP, since they are
order-independent as well (exchange is allowed). We use l to range over parameter names. These are constants, and
are thus not affected by α-renaming. Formally, ρ is a record that maps parameter names to channels used inside P,
i.e., ρ = {li = x i }i . We omit curly brackets for records in the remainder when they are clear from the context, e.g., as
in phl 1 = x, l 2 = yi. Given a record ρ = {li = x i }i , we call the set {li }i the preimage of ρ and the set {x i } the image
5

of ρ. An abstraction (ρ)P binds all names in the image of ρ in P. We require abstractions to be closed with respect to
channels, in the sense that the image of ρ needs to be exactly the set of all free channel names in P.
Dual to higher-order output, the higher-order input term x(p).Q receives an abstraction over channel x and stores it
in the process variable p, which can be used in the continuation Q.
Abstractions stored in a process variable p can be invoked (we also say run) using term phρi, where ρ are the actual
named parameters to be used by the process.
We purposefully chose a minimalistic syntax for CHOP, for economy of the calculus. For example, our process
output term has no continuation, but we will see in section 5.1 that an equivalent construct with continuation can be
easily given as syntax sugar. The continuation in the process input term x(p).Q is necessary for scoping, because p is
bound in Q. The syntax of the run term is clearly minimal.
Remark 1. The choice of having (named) parameters and abstractions is justified by the desire to use received processes
to implement behaviours. For example, we may want to receive a channel and then use a process to implement the necessary
behaviour on that channel: x(y).x(p).phl = yi.
A different way of achieving the same result would be to support the communication of processes with free names (not
abstractions), and then allow run terms to dynamically rename free names of received processes. For example, if we knew
from typing that any process received for p above has z as free names, we could write x(y).x(p).phx = yi.
Such a dynamic binding mechanism would make our syntax simpler, since invocations would simply be phσ i (σ is
a name substitution) and the higher-order output term would be x[P]. However, dynamic binding is undesirable in a
programming model, since the scope of free names can change due to higher-order communications. The reader unfamiliar
with dynamic binding may consult (Sangiorgi and Walker 2001, p. 376) for a discussion of this issue in HOπ .
Typing. We now move to typing. The most influential change is actually caused by the run term, so we start from
there. How should we type a term phρi? The rule should look like the following informal template (where ?? are
unknown).
??
` phρi :: ??
Since p stores a process (abstraction), and processes communicate over channels, we should be able to type it with
some environment Γ. But what Γ should we use? This depends on what abstraction is stored in variable p. Such way of
reasoning immediately calls for the introduction of a new higher-order context, which we denote with Θ, where we
store typing information on process variables. This is the usual typing of variables seen in many calculi, but instead of
value types, we store process types. The type of a process in CP is evident: it is a context Γ. So a higher-order context Θ
associates process variables to process types Γ, i.e., Θ = p1 : Γ1 , . . . , pn : Γn . Notice, however, that since each pi is going
to be instantiated by an abstraction, we are not typing channels in each Γi , but the names of formal parameters (l). Thus
we can write the following rule.
p : Γ ` phρi :: Γρ

Id

Rule Id says that if we run p by providing all the necessary channel parameters (collected in ρ) for running the
abstraction that it contains, then we implement exactly the session types that type the code that may be contained in p
(modulo the renaming of the formal parameters performed with ρ, hence the Γρ). Notice that we use all our available
“resources”—the channel names in the image of ρ—to run p, passing them as parameters. This ensures linearity.
Our rule means, however, that we have changed the shape of typing judgements from that in CP, since we have
added Θ. Luckily, adapting all rules in CP to the new format is straightforward: we just need to distribute Θ over
6

premises, respecting linearity of process variables. For example, rule Cut is adapted as follows.
Θ ` P :: Γ, x : A

Θ 0 ` Q :: ∆, y : A⊥

Θ, Θ 0 ` (νx Ay) (P | Q) :: Γ, ∆

Cut

The full set of adapted rules is given in the next section. We read the judgement Θ ` P :: Γ as “P uses process variables
according to Θ and channels according to Γ”. Observe that some channel behaviour may not be implemented by P itself,
but it could instead be delegated to some invocations of process variables as we exemplified before.
Now that we know how to type process variables, we can move on to typing process inputs and outputs. Before we
do it, though, we need to extend the syntax of types to capture the sending and receiving of processes, as follows.
...

A, B, C ::=

[Γ]

send process of type Γ

hΓi

receive process of type Γ

We can now type a process input.
Θ, p : ∆ ` P :: Γ
hi
Θ ` x(p).P :: Γ, x : h∆i
Rule hi says that if we receive a process of type ∆ over channel x and store it in variable p, we can use variable p later in
the continuation Q assuming that it implements ∆. The type for the channel x is h∆i. If we think in terms of channels,
this type means that we receive a process of type ∆. If we think in terms of proof theory, it means that we are assuming
that there exists of a proof of ∆.
The rule for typing a process output follows.
Θ ` P :: Γρ
[]
Θ ` x[(ρ)P] :: x : [Γ]
Rule [] should be self-explanatory by now. It says that if we send a process of type P over channel x and P implements
Γ, then x has type [Γ]. Note that we allow (actually, we ensure, because of linearity) P to use the process variables
available in the context (Θ). This is not an arbitrary choice made just to increase expressivity of the calculus: we will
see in section 3 that it follows naturally from the notion of η-expansion of CLL.

Usage and Semantics. Intuitively, the type constructors [] and hi are dual of each other: for any Γ, hΓi means that we
need a proof of Γ, while [Γ] means that we provide such a proof. So we extend duality as follows.
[Γ]⊥

=

hΓi

hΓi ⊥

=

[Γ]

This allows us to compose processes that make use of the higher-order input and output primitives. For example,
consider the following cut.
Θ 0, p : ∆ ` Q :: Γ
hi
` x(p).Q :: Γ, y : h∆i
Cut
Θ, Θ 0 ` (νx [∆]y) (x[(ρ)P] | x(p).Q) :: Γ

Θ ` P :: ∆ρ
[]
Θ ` x[(ρ)P] :: x : [∆]

Θ0

Let us now consider what the operational semantics of term (νx [∆]y) (x[(ρ)P] | x(p).Q) should be. Intuitively, we
would expect it to reduce to something like Q with each occurrence of p replaced by P. Indeed, in HOπ (adapted to our
7

syntax), we would have (νx [∆]y) (x[(ρ)P] | x(p).Q) −→ Q {(ρ)P/p}. In our setting, using this kind of “immediate” substitution can be undesirable for two reasons. First, it is impractical: in practice, substitutions are typically implemented
by replacing subterms as needed (possibly in a delayed fashion), rather than blind immediate rewriting (Wadsworth
1971). Second, it is theoretically inconvenient: in our example of cut reduction in multiplicative CP, we could prove that
the reductum is well-typed just by looking at the premises of the cut (more precisely, using them to write a new smaller
proof); but here it is not possible, since our premises do not talk about Q {(ρ)P/p}.
We deal with both issues by introducing a notion of explicit substitution for process variables. The syntax of an
explicit substitution is Q[p:= (ρ)P], read “let p be (ρ)P in Q”. We type explicit substitutions with the rule below.
Θ ` P :: ∆ρ Θ 0, p : ∆ ` Q :: Γ
Chop
Θ, Θ 0 ` Q[p:= (ρ)P] :: Γ
Rule Chop allows us to replace p with (ρ)P in Q, provided that P and q have compatible typing (up to the formal named
parameters). If you think in terms of processes, CHOP stands for “Cut for Higher-Order Processes”. If you think in
terms of logic, CHOP stands for “Cut for Higher-Order Proofs”. The idea is that a variable p stands for a “hole” in a
proof, which has to be filled as expected by the type for p.
Observe that our previous proof for typing (νx [∆]y) (x[(ρ)P] | x(p).Q) has exactly the same premises needed for
rule Chop. This means that we can derive the following reduction rule.
(νx [∆]y) (x[(ρ)P] | x(p).Q) −→ Q[p:= (ρ)P]
The reduction above models exactly what we would expect in a higher-order process calculus, but using an explicit
substitution. In section 3, we will see that rule Chop allows for sound proof rewrites that yield the expected semantics
of explicit substitutions for higher-order processes. In particular, explicit substitutions can be propagated inside of
terms, as illustrated by the following example reduction.
(x(y).Q)[p:= (ρ)P] −→ x(y).(Q[p:= (ρ)P])
Also, when a substitution reaches its target process variable, it replaces it.
phρi[p:= (ρ 0 )P] −→ P {ρ ◦ ρ 0 −1 }
Above, we abuse notation and interpret ρ as functions that map labels to names, and then ◦ is standard function
composition.
This ends our overview of the intuition behind the journey from CP to CHOP. In the next sections, we move to the
formal presentation of CHOP, its metatheory, extensions, and further discussions.

3

CLASSICAL HIGHER-ORDER PROCESSES (CHOP)

We formally introduce the calculus of Classical Higher-Order Processes (CHOP). Technically, CHOP is a strict generalisation of the calculus of Classical Processes (CP) by Wadler (2014). We refer to the latest version of CP, given in
(Carbone et al. 2016).
8

Processes. In CHOP, programs are processes (P,Q,R,. . .) that communicate over channels (x,y,. . .). The syntax of
processes is the following. Some terms include types (A, B, C, . . .), which we present afterwards.
P, Q, R ::=

x[y].(P | Q)

output a channel

x(y).P

input a channel

x[inl].P

select left

x[inr].P

select right

x .case(P, Q)

offer a choice

?x[y].P

client request

!x(y).P

server accept

x[A].P

output a type

x(X ).P

input a type

x[(ρ)P]

higher-order output

x(p).P

higher-order input

phρi

run

x[]

close

x().P

wait

x .case()

empty offer

x → yA

link

(νx Ay) (P | Q)

parallel composition

P[q:= (ρ)Q]

explicit substitution

We are already familiar with some terms, from the overview in section 2. Here, we briefly describe the meaning of each.
Term x[y].(P | Q) sends y over x, and then continues as P and Q in parallel. Dually, term x(y).P receives y over
x. In both these terms, y is bound in the continuation P. Term x[inl].P selects the left branch of an offer available
over x. Likewise, x[inr].P selects the right branch. Dually, term x .case(P, Q) offers a choice between P (left branch)
and Q (right branch) over x. Term ?x[y].P sends y to a server (an always-available replicated process) available over
x, and then proceeds as P. Dually, term !x(y).P is a replicated server waiting for requests to create new instances on
x (the instance will then communicate with the client over y). Name y is bound in both the client and server terms.
Terms x[A].P and x(X ).P enable polymorphism. Term x[A].P sends type A over x and proceeds as P; while term x(X ).P
receives a type over x and then proceeds as P, where X is bound in P. Term x[(ρ)P] sends the (process) abstraction
(ρ)P over x, where ρ is a record that maps the parameter names (ranged over by l) of the abstraction to free names in
P. Dually, term x(p).P receives an abstraction over x and stores it in variable p, to be used in the continuation P (p is
bound in P). A term phρi runs the process stored inside of variable p, instantiating its named parameters according to ρ.
Term x[], or empty output, sends over x the message that the channel is being closed and closes it. Term x().P waits
for one of such close messages on x and then continues as P. A link term x → y A acts as a forwarding proxy: inputs
along x are forwarded as outputs to y and vice versa, any number of times (as dictated by the protocol A). The parallel
composition term (νx Ay) (P | Q) connects the channels x at process P and y at process Q to form a session, enabling
the two processes to communicate. The names x and y are bound, respectively, in P and Q. The type A describes the
behaviour that the processes will follow when communicating. Finally, the explicit substitution term P[q:= (ρ)Q] stores
the abstraction (ρ)Q in variable q, and binds the latter in P.
9

α-conversion works as usual. Following the intuition that invocation terms use named parameters, bound names
inside of ρ in terms phρi are also affected by α-conversion. For example, these two processes are α-equivalent:
x(y).phl = yi and x(z).phl = zi. Parameters are technically important: in the second process, if we did not rename y
to z in the substitution, y would become a free name but it was a bound name in the first process! This is the same
mechanism behind α-equivalence for abstraction invocation in HOπ , just extended to our named parameters. We
consider processes up to α-equivalence in the remainder.

Types and environments. There are two kinds of types in CHOP. Session types, ranged over by A, B, C, . . ., are used
to type channels, and process types, ranged over by Γ, ∆, . . ., are used to type processes.
We inherit all the session types of CP, which correspond to propositions in CLL, and have also our new ones for
typing communication of processes. We range over atomic propositions in session types with X , Y . The syntax of types
is given in the following, along with a brief description of each case. We use s to range over parameter names (l) and
channels (x).
A, B, C ::=

A⊗B

send A, proceed as B

AOB

receive A, proceed as B

A⊕B

select A or B

ANB

offer choice between A and B

0

unit for ⊕

>

Γ, ∆ ::=

unit for N

1

unit for ⊗

⊥
?A

unit for O

!A

server accept

∃X .A

existential

∀X .A

universal

X

atomic proposition

X⊥

dual of atomic proposition

[Γ]

send process of type Γ

hΓi

receive process of type Γ

s 1 : A 1 , . . . , s n : An

process type

client request

In ∃X .A and ∀X .A, type variable X is bound in A. We write ftv(A) for the set of free type variables in A. We ignore
the order of associations in process types (exchange is allowed). Whenever we write Γ, ∆, we assume that Γ and ∆ are
disjoint (share no channel names). We write (si : Ai )i as an abbreviation of s 1 : A1 , . . . , sn : An . Typing will ensure that
all keys in an environment are of the same kind (either parameter names or channels).
Just like CP, CHOP uses the standard notion of duality from linear logic to check that session types are compatible.
As described in section 2.2, we extend duality to deal with our new session types, [Γ] and hΓi. Formally, we write A⊥
10

for the type dual to A, defined inductively as follows.
(X )⊥

=

X⊥

(A ⊗

B)⊥

=

A⊥

(X ⊥ )⊥

=

X

B)⊥

(A ⊕

B)⊥

=

0⊥

=

A⊥ NB ⊥

=

A⊥ ⊗ B ⊥

(ANB)⊥

=

A⊥ ⊕ B ⊥

1⊥

>

>⊥

=

0

=

⊥

⊥⊥

=

1

(?A)⊥

=

!A

(!A)⊥

=

?A

(∃X .A)⊥

=

∀X .A⊥

(∀X .A)⊥

=

∃X .A⊥

[Θ; Γ]⊥

=

hΘ; Γi

hΘ; Γi ⊥

=

[Θ; Γ]

O

B⊥

(A O

Duality is an involution, i.e., (A⊥ )⊥ = A.
A process environment Θ associates process variables to process types.
Θ ::=

p1 : Γ1 , . . . , pn : Γn

process environment

We write · for the empty process environment (no associations). Similarly to process types, we allow for exchange in
process environments and require all process variables in a process environment to be distinct.

Typing. Typing judgements in CHOP have the form Θ ` P :: Γ, which reads “process P uses process variables
according to Θ and channels according to Γ”. We omit Θ in judgements when it is empty (·). The rules for deriving
judgements are displayed in fig. 2.
Typing rules associate types to channels by looking at how the channel is used in process terms, as expected. They
should be unsurprising by now, after our discussion in section 2.2. We just make a few observations for the reader
unfamiliar with CP and/or linear logic. Rule Axiom types a link between x and y by requiring that the types of x and y
are the dual of each other. This ensures that any message on x can be safely forwarded to y, and vice versa. All rules for
typing channels enforce linear usage aside for client requests (typed with the exponential connective ?), for which
contraction and weakening are allowed. Contraction (rule Contract) allows for having multiple client requests for
the same server channel, and weakening (rule Weaken) allows for having a client that does not use a server. Rule !
types a server, where ?Γ denotes that all session types in Γ must be client requests, i.e., ?Γ ::= x 1 : ?A1 , . . . , x n : ?An .
A server must be executable any number of times, since it does not know how many client requests it will have to
support. This is guaranteed by requiring that all resources used by the server are acquired by communicating with the
client (according to protocol A) and with other servers (?Γ).
The rules for typing higher-order terms have already been discussed in section 2.2. We can now substantiate our
remark on the design of rule [] made in the same section, which allows the sent abstraction to use process variables
available in the context of the sender (Θ). It is well-known that restricting rule Axiom to atomic propositions in
CLL does not reduce expressivity, because the general Axiom can be reconstructed as an admissible rule. A cut-free
derivation of ` x → y A :: x : A⊥ , y : A corresponds to the η-expansion of the link term x → y A , and η-expansion is also
a convenient tool for the elegant formulation of multiparty sessions in CP, as shown by (Carbone et al. 2016). That the
general Axiom is admissible is thus an important property of CP, and preserving this property is desirable in CHOP for
the same reasons. The following proof shows the new case of η-expansion for higher-order communications introduced
11

Θ ` P :: Γ, x : A
` x → y A :: x : A⊥ , y : A

Axiom

Θ, Θ 0 ` (νx Ay) (P | Q) :: Γ, ∆

Θ ` P :: Γ, y : A Θ 0 ` Q :: ∆, x : B
⊗
Θ, Θ 0 ` x[y].(P | Q) :: Γ, ∆, x : A ⊗ B
Θ ` P :: Γ, x : A
⊕1
Θ ` x[inl].P :: Γ, x : A ⊕ B

Θ 0 ` Q :: ∆, y : A⊥

Θ ` P :: Γ, y : A, x : B
O
Θ ` x(y).P :: Γ, x : A O B

Θ ` P :: Γ, x : B
⊕2
Θ ` x[inr].P :: Γ, x : A ⊕ B

Θ ` P :: Γ, y : A
?
Θ ` ?x[y].P :: Γ, x : ?A

Cut

Θ ` P :: Γ, x : A Θ ` Q :: Γ, x : B
N
Θ ` x .case(P, Q) :: Γ, x : A N B

` P :: ?Γ, y : A
!
` !x(y).P :: ?Γ, x : !A

Θ ` P :: Γ, x : B{A/X }
∃
Θ ` x[A].P :: Γ, x : ∃X .B

Θ ` P :: Γ, x : B X < ftv(Θ) ∪ ftv(Γ)
∀
Θ ` x(X ).P :: Γ, x : ∀X .B

Θ ` P :: Γ
Weaken
Θ ` P :: Γ, x : ?A

Θ ` P :: Γ, y : ?A, z : ?A
Contract
Θ ` P {x/y, x/z} :: Γ, x : ?A

` x[] :: x : 1

1

Θ ` P :: Γ
⊥
Θ ` x().P :: Γ, x : ⊥

p : Γ ` phρi :: Γρ

Id

(no rule for 0)

Θ ` x .case() :: Γ, x : >

>

Θ ` P :: ∆ρ Θ 0, p : ∆ ` Q :: Γ
Chop
Θ, Θ 0 ` Q[p:= (ρ)P] :: Γ
Θ, p : ∆ ` P :: Γ
hi
Θ ` x(p).P :: Γ, x : h∆i

Θ ` P :: Γρ
[]
Θ ` x[(ρ)P] :: x : [Γ]

Fig. 2. CHOP, Typing Rules.

by our new types, which yields the expansion x → y [∆] −→ x(p).x[(ρ)phρi] (where ρ captures all the names in ∆) .
Id
p : ∆ ` phρi :: ∆ρ
[]
p : ∆ ` x[(ρ)phρi] :: x : [∆]
hi
` x(p).x[(ρ)phρi] :: x : h∆i, x : [∆]
Notice that without allowing the sent abstraction to use the linear process variables available to the sender, the derivation
would be invalid. This also shows that rule Id is in harmony with our rules for higher-order input and output. We still
have to prove that our rules are in harmony also with rule Cut, as usual, in order to obtain cut elimination. We prove
this in section 3.2, and establish a metatheory for CHOP in section 4.
3.1

Example

We illustrate the expressivity of CHOP by implementing a cloud server for running applications that require a database.
The idea is that clients are able to choose between two options: run both the application and the database it needs in
the server, or run just the application in the server and connect it to an externally-provided database (which we could
imagine is run somewhere else in the cloud).
12

A cloud server. The process for the cloud server follows. We assume that A is the protocol (left unspecified) that
applications have to use in order to communicate with databases, and l is the named parameter used by both abstractions
to represent this shared connection (the parameter names may be different, we do this only for a simpler presentation).
We also let applications and databases access some external services, e.g., loggers, through the parameters l and m
respectively. We write l = x for l 1 = x 1 , . . . , ln = x n .
!cs(x). x .case( x(x 0 ).x(app).x 0 (db).(νz Aw) (apphl = z, l = ui | dbhl = w, m = vi),
⊥

x(extdb).x(app).(νz Aw) (apphl = z, l = ui | extdb → w A )

)

The cloud server waits for client requests on channel cs. Then, it communicates with the client on the established
channel x. It offers the options that we mentioned through a choice, respectively with the left and right branches. In
the left branch, we first receive an auxiliary channel x 0 . We then receive the application app on x and the database db
on x 0 . Then, we compose and run app and db in parallel, connecting them through the endpoints z and w. In the right
branch, we first receive a channel extdb for communicating with the external database, and then receive the application
⊥

app. Then, we compose app with a link term extdb → w A , which connects the application to the external database.

Typing the cloud server. We now illustrate how to use our typing rules to prove that the cloud server is well-typed.
Let ?Γ = (li : ?Ai )i , ?∆ = (mi : Bi )i , ρ = {l = z, l = u}, and ρ 0 = {l = w, m = v}. For readability, we first type the left
and right branches in the choice offered through x. Here is the proof for the left branch.
app : (?Γ, l : A) ` apphρi :: ?Γρ, z : A

Id

Id

db : (?∆, l : A⊥ ) ` dbhρ 0 i :: ?∆ρ 0, w : A⊥

Cut

app : (?Γ, l : A), db : (?∆, l : A⊥ ) ` (νz Aw) (apphρi | dbhρ 0 i) :: ?Γρ, ?∆ρ 0
app : (?Γ, l : A) ` x 0 (db).(νz Aw) (apphρi | dbhρ 0 i) :: ?Γρ, ?∆ρ 0, x 0 : h?∆, l : A⊥ i

hi

` x(app).x 0 (db).(νz Aw) (apphρi | dbhρ 0 i) :: ?Γρ, ?∆ρ 0, x 0 : h?∆, l : A⊥ i, x : h?Γ, l : Ai

hi

` x(x 0 ).x(app).x 0 (db).(νz Aw) (apphρi | dbhρ 0 i) :: ?Γρ, ?∆ρ 0, x : h?∆, l : A⊥ i O h?Γ, l : Ai

O

And this is the proof for the right branch.
app : (?Γ, l : A) ` apphρi :: ?Γρ, z : A

Id

⊥

` extdb → w A :: extdb : A, w : A⊥

Cut

⊥

app : (?Γ, l : A) ` (νz Aw) (apphρi | extdb → w A ) :: ?Γρ, extdb : A
⊥

` x(app).(νz Aw) (apphρi | extdb → w A ) :: ?Γρ, extdb : A, x : h?Γ, l : Ai
` x(extdb).x(app).(νz Aw) (apphρi | dbhρ 0 i) :: ?Γρ, x : A O h?Γ, l : Ai

Axiom

hi
O

Now that we have proofs for the two branches, we can use them to type the entire cloud server. Let L and R be the
two proofs above, respectively, and P L and P R the processes that they type (the left and right branches in the cloud
server). Then, we type the cloud server as follows.
L R
N

` x .case(P L , P R ) :: ?Γρ, ?∆ρ 0, x : h?∆, l : A⊥ i O h?Γ, l : Ai N (A O h?Γ, l : Ai)

 !
` !cs(x). x .case(P L , P R ) :: ?Γρ, ?∆ρ 0, cs : ! h?∆, l : A⊥ i O h?Γ, l : Ai N (A O h?Γ, l : Ai)
The types for our cloud server follows the intuition that we initially discussed for this example. The typing derivation
also illustrates the interplay between our new features (process mobility and the usage of process variables) with the
other features of the calculus—in this example: channel mobility, exponentials (replicated services), choices, and links.
13

A generic improvement. The code of our cloud server implementation would not depend on how clients and database
communicate, were it not for the hardcoded protocol A. We can get rid of the hardcoded A and reach a generic
implementation using polymorphism. Here is the improved implementation, where we box the improvements.
!cs(x). x(X ). x .case( x(x 0 ).x(app).x 0 (db).(νz X w) (apphρi | db hρ 0 i),
⊥
x(extdb).x(app).(νz X w) (apphρi | extdb → w X )

)

In the improved cloud server, the client must also send us the protocol X that the application will use to communicate
with the database. The cloud server is thus now generic, and the type of channel cs is the following.



 
h?∆, l : X ⊥ i O h?Γ, l : X i N X O h?Γ, l : X i
! ∀X .
Here is the proof.
L{X /A} R{X /A}
N

` x .case(P L , P R ) :: ?Γρ, ?∆ρ 0, x : h?∆, l : X ⊥ i O h?Γ, l : X i N (X O h?Γ, l : X i)

 ∀
` x(X ). x .case(P L , P R ) :: ?Γρ, ?∆ρ 0, x : ∀X . h?∆, l : X ⊥ i O h?Γ, l : X i N (X O h?Γ, l : X i)

 !
` !cs(x). x(X ). x .case(P L , P R ) :: ?Γρ, ?∆ρ 0, cs : ! ∀X . h?∆, l : X ⊥ i O h?Γ, l : X i N (X O h?Γ, l : X i)
The proofs L{X /A} and R{X /A} used above are as L and R respectively, but wherever we had A we now have X .
The interplay between type variables and process variables merits illustration, so we show R{X /A} in full.
app : (?Γ, l : X ) ` apphρi :: ?Γρ, z : X

Id

⊥

` extdb → w X :: extdb : X , w : X ⊥

Cut

⊥

app : (?Γ, l : X ) ` (νz X w) (apphρi | extdb → w X ) :: ?Γρ, extdb : X
⊥

` x(app).(νz X w) (apphρi | extdb → w X ) :: ?Γρ, extdb : X , x : h?Γ, l : X i
` x(extdb).x(app).(νz X w) (apphρi | dbhρ 0 i) :: ?Γρ, x : X O h?Γ, l : X i

Axiom

hi
O

Observe the application of rule hi in the proof. If we read it bottom-up, we are moving the type variable X from the
typing of a channel in the conclusion—x : X O h?Γ, l : X i—to the typing of a process in the premise—app : (?Γ, l : X ).
This is then carried over to the application of Id, which is thus able to type the usage of a process variable that is generic
on the behaviour that will be enacted.

3.2

Semantics

To give a semantics to CHOP, we follow the approach that we outlined in section 2.2: we derive term reductions
(denoted −→) and equivalences (denoted ≡) from sound proof transformations. We distinguish between principal
reductions, which reduce cuts and chops that act directly on their premises (e.g., compatible output and input terms),
and reductions that arise from commuting conversions, which just “push” cuts or chops up a proof. The full proofs of
principal reductions related to process mobility (the hallmark of CHOP) are displayed in fig. 3, and a set of representative
commuting conversions are displayed in fig. 4 (the dashed lines are just visual separators between different commuting
conversions, for readability). The reader familiar with linear logic will recognise that principal reductions follow the
same methodology of principal cut reductions in CLL, but now extended to our new cases and also applied to the
principal cases that we get for our new rule Chop.
14

Θ 0, p : ∆ ` Q :: Γ
hi
Θ ` P :: ∆ρ Θ 0, p : ∆ ` Q :: Γ
Θ 0 ` x(p).Q :: Γ, y : h∆i
−→
Chop
Cut
Θ, Θ 0 ` Q[p:= (ρ)P] :: Γ
Θ, Θ 0 ` (νx [∆]y) (x[(ρ)P] | x(p).Q) :: Γ

Θ ` P :: ∆ρ
[]
Θ ` x[(ρ)P] :: x : [∆]

Id
Θ ` P :: Γρ 0 p : Γ ` phρi :: Γρ
0 −1
Chop −→ Θ ` P {ρ ◦ ρ } :: Γρ
Θ ` phρi[p:= (ρ 0 )P] :: Γρ
Fig. 3. CHOP, Principal Proof Reductions for Process Mobility.

Θ 0, r : ∆ ` P :: Γ, x : A

Θ 00 ` Q :: Γ 0, y : A⊥

Θ ` R :: ∆ρ

Θ, r : ∆ ` (νx Ay) (P | Q) :: Γ, Γ 0

Chop
Θ, Θ 0, Θ 00 ` (νx Ay) (P | Q) [r := (ρ)R] :: Γ, Γ 0

Cut
−→



Θ ` R :: ∆ρ Θ 0, r : ∆ ` P :: Γ, x : A
Chop
Θ, Θ 0 ` P[r := (ρ)R] :: Γ, x : A

Θ 00 ` Q :: Γ 0, y : A⊥

Θ, Θ 0, Θ 00 ` (νx Ay) (P[r := (ρ)R] | Q) :: Γ, Γ 0

Cut

Θ 0, r : ∆ ` P :: Γ, y : A Θ 00 ` Q :: Γ 0, x : B
⊗
Θ ` R :: ∆ρ Θ 0, Θ 00, r : ∆ ` x[y].(P | Q) :: Γ, Γ 0, x : A ⊗ B
−→
Chop
Θ, Θ 0, Θ 00 ` (x[y].(P | Q)) [r := (ρ)R] :: Γ, Γ 0, x : A ⊗ B
Θ ` R :: ∆ρ Θ 0, r : ∆ ` P :: Γ, y : A
Chop
Θ, Θ 0 ` P[r := (ρ)R] :: Γ, y : A
Θ 00 ` Q :: Γ 0, x : B
⊗
0
00
Θ, Θ , Θ ` x[y].(P[r := (ρ)R] | Q) :: Γ, Γ 0, x : A ⊗ B
Θ 0, r : ∆ ` P :: Γ, y : A, x : B
O
Θ ` R :: ∆ρ
: ∆ ` x(y).P :: Γ, x : A O B
−→
Chop
Θ, Θ 0 ` (x(y).P) [r := (ρ)R] :: Γ, x : A O B
Θ 0, r

Θ ` R :: ∆ρ Θ 0, r : ∆ ` P :: Γ, y : A, x : B
Chop
Θ, Θ 0 ` P[r := (ρ)R] :: Γ, x : A O B
O
Θ, Θ 0 ` x(y). (P[r := (ρ)R]) :: Γ, x : A O B
Fig. 4. CHOP, Representative Commuting Conversions for Explicit Substitutions.

The first reduction in fig. 3 shows how a process communication is reduced to an explicit substitution of the
transmitted process at the receiver. The second reduction shows how an explicit substitution replaces a process
invocation. The reductions in fig. 4 illustrate how explicit substitutions float inside of terms.
The full sets of reductions and equivalences supported by CHOP are displayed in fig. 5 (principal reductions), fig. 6
(η-expansion), and fig. 7 (commuting conversions and structural equivalences). We use the following notation: fn(P) is
the set of free names (channels and process variables) in P; n(∆) is the set of names (actually labels, in the case of the
15

(νx A ⊗B y) (x[x 0 ].(P | Q) | y(y 0 ).R) −→ (νx 0Ay 0 ) (P | (νx B y) (Q | R))
(νx A ⊕B y) (x[inl].P | y.case(Q, R)) −→ (νx Ay) (P | Q)
(νx A ⊕B y) (x[inr].P | y.case(Q, R)) −→ (νx Ay) (P | R)
(νx ?Ay) (?x[u].Q | !y(v).P) −→ (νu Av) (P | Q)
(νx ?Ay) (P | !y(v).Q) −→ P

?A
(νx y) (P {x/x 0, x/x 00 } | !y(v).Q) −→ (νx 0 ?Ay 0 ) (νx 00 ?Ay 00 ) (P | !y 00 (v).Q) | !y 0 (v).Q
(νx ∃X .B y) (x[A].P | y(X ).Q) −→ (νx B {A/X }y) (P | Q {A/X })
(no rule for 0 with >)
(νx 1y) (x[] | y().P) −→ P
(νx [Σ;∆]y) (x[(ρ)P] | x(p).Q) −→ Q[p:= (ρ)P]
phρi[p:= (ρ)P] −→ P
(νx X y) (w → x X | P) −→ P {w/y}
Fig. 5. CHOP, Principal Reductions.

x → y A ⊗B
x → y A ⊕B
x → y ?A
x → y [Σ;∆]

−→
−→
−→
−→

x(u).y[v].(u → v A | x → y B )
x → y1
A
B
x .case(y[inl].x → y , y[inr].x → y )
x → y0
A
!x(u).?y[v].u → v
x → y ∃X .A
x(p).y[(ρ)phρi] if dom(ρ) = n(Σ) ∪ n(∆)

−→
−→
−→

x().y[]
x .case()
x(X ).y[X ].x → y A

Fig. 6. CHOP, η-expansions.

η-expansion in fig. 6) associated to types in ∆; and dom(ρ) is the preimage of ρ (the defined domain of ρ, interpreting it
as a partial function, i.e., the set of labels associated to values in the record ρ).
We use a simplified form of the second reduction proven in fig. 3: phρi[p:= (ρ)P] −→ P. This is obtained by assuming
that α-conversion is used on the abstraction (ρ)P until all the names bound by the abstraction term (ρ) match exactly
the names used by the invocation (phρi).
An alternative to having η-expansion is to generalise our reduction (νx X y) (w → x X | P) −→ P {w/y}, which is
restricted to atomic propositions X , to the form (νx Ay) (w → x A | P) −→ P {w/y}, which is not. Both are sound in
CHOP, and the choice on which one should be adopted thus depends on other criteria. Here we choose to use the
formulation based on η-expansion, because it will be useful later in our extension to multiparty sessions (section 5.2).
In the remainder, we allow reductions to silently apply equivalences. We also allow reductions to happen inside of
cuts and chops, as formalised in the following.
(νx Ay) (P1 | Q)

−→

(νx Ay) (P2 | Q)

| Q1)

−→

(νx Ay) (P

Q 1 [p:= (ρ)P]

−→

Q 2 [p:= (ρ)P]

(νx Ay) (P

3.3

| Q2)

if P1 −→ P2
if Q 1 −→ Q 2
if Q 1 −→ Q 2

Example, semantics

Take the improved cloud server given in section 3.1, which we write here again for convenience and call Psrv .
Psrv = !cs(x). x(X ). x .case( x(x 0 ).x(app).x 0 (db).(νz X w) (apphρi | dbhρ 0 i),
def

⊥

x(extdb).x(app).(νz X w) (apphρi | extdb → w X )
16

)

⊥

x → yA ≡ y → x A
⊥
A
(νz w) (P | Q) ≡ (νw A z) (Q | P)


(νz Aw) (νx B y) (P | Q) | R
(νz Aw) (x[y].(P | Q)
(νz Aw) (x[y].(P | Q)
(νz Aw) (x(y).P
(νz Aw) (x[inl].P
(νz Aw) (x[inr].P
A
(νz w) (x .case(P, Q)
(νz Aw) (!x(y).P
(νz Aw) (?x[y].P
(νz Aw) (x[B].P
(νz Aw) (x(X ).P
(νz Aw) (x().P
(νz Aw) (x .case()




|
|
|
|
|
|
|
|
|
|
|
|

≡ (νx B y) P | (νz Aw) (Q | R)



R) −→ x[y].((νz Aw) (P | R) | Q)
if z ∈ fn(P)
R) −→ x[y].(P | (νz Aw) (Q | R))q
if z ∈ fn(Q)
Q) −→ x(y).(νz Aw) (P | Q)
Q) −→ x[inl].(νz Aw) (P | Q)
Q) −→ x[inr].(νz Aw) (P | Q)
R) −→ x .case((νz Aw) (P | R), (νz Aw) (Q | R))
Q) −→ !x(y).(νz Aw) (P | Q)
Q) −→ ?x[y].(νz Aw) (P | Q)
Q) −→ x[B].(νz Aw) (P | Q)
Q) −→ x(X ).(νz Aw) (P | Q)
Q) −→ x().(νz Aw) (P | Q)
Q) −→ x .case()

(νx Ay) (P | Q) [r := (ρ)R] −→ (νx Ay) (P[r := (ρ)R] | Q)

(νx Ay) (P | Q) [r := (ρ)R] −→ (νx Ay) (P | Q[r := (ρ)R])
(x[y].(P | Q)) [r := (ρ)R] −→ x[y].(P[r := R] | Q)
(x[y].(P | Q)) [r := (ρ)R] −→ x[y].(P | Q[r := (ρ)R])
(x(y).P) [r := (ρ)R] −→ x(y). (P[r := (ρ)R])
(x[inl].P)[r := (ρ)R] −→ x[inl].(P[r := (ρ)R])
(x[inr].P)[r := (ρ)R] −→ x[inr].(P[r := (ρ)R])
(x .case(P, Q)) [r := (ρ)R] −→ x .case(P[r := (ρ)R], Q[r := (ρ)R])
(?x[y].P) [r := (ρ)R] −→ ?x[y].(P[r := (ρ)R])
(x[A].P) [r := (ρ)R] −→ x[A].(P[r := (ρ)R])
(x(X ).P) [r := (ρ)R] −→ x(X ).(P[r := (ρ)R])
(x[(ρ 0 )P]) [r := (ρ)R] −→ x[(ρ 0 )(P[r := (ρ)R])]
(x(p).P) [r := (ρ)R] −→ x(p).(P[r := (ρ)R])
(x().P) [r := (ρ)R] −→ x().(P[r := (ρ)R])
(no rule for 0)

if r ∈ fn(P)
if r ∈ fn(Q)
if r ∈ fn(P)
if r ∈ fn(Q)

Fig. 7. CHOP, Equivalences and Commuting Conversions.

Here is a simple compatible client, Pcl i . It uses the second option: connecting the application in the cloud server
to an existing database. We run this database in the client itself (Pdb ). This makes sense in many practical scenarios,
where the client wants to maintain ownership of its data but also to delegate heavy computational tasks to the cloud.
Type A is the protocol, left unspecified, between the application sent by the client (Papp ) and its database.
Pcl i = ?cc[y].y[A].y[inr].y[d].(Pdb | y[(ρ)Papp ])
def

Process Pcl i implements on channel cc (for cloud client) the dual type of that implemented by Psrv on channel cs (for
cloud server), discussed in section 3.1. So we can compose them in parallel (we omit types at restrictions, for brevity).
Psys = (νcc cs) (Pcli | Psrv )
def

17

The semantics of our system Psys depends on whether Pdb uses channel cc (to use the cloud server itself) or not. If it
does, then we have to replicate Psrv , otherwise we have to execute a single instance of it. Let us assume that we need a
single instance (Pdb does not use cc). Then we have the following reduction chain for the first three communications
(invocation of the server, communication of the protocol A, right selection).
⊥

Psys −→−→−→ (νyx) (y[d].(Pdb | y[(ρ)Papp ]) | x(extdb).x(app).(νz Aw) (apphρi | extdb → w A ))
Notice that the server now knows the protocol A between the application and the database. A further reduction gives
us the following process.



⊥
−→ (νd extdb) Pdb | (νyx) y[(ρ)Papp ] | x(app).(νz Aw) (apphρi | extdb → w A )
We can now reduce the communication between y and x, so that now Papp is moved from the client to server, and
reduce the resulting explicit substitution at the server, as follows.


⊥
−→−→ (νd extdb) Pdb | (νz Aw) (Papp | extdb → w A )
So we now have that the database of the client communicates with the application in the server, as we originally
intended.
4

METATHEORY

We now move to the metatheoretical properties of CHOP.
4.1

Type preservation

Since all reductions and equivalences in CHOP are derived from type-preserving proof transformations, we immediately
get a type preservation result for both.
Theorem 4.1 (Type preservation). Let Θ ` P :: Γ. Then,
• P ≡ Q for some Q implies Θ ` Q :: Γ, and
• P −→ Q for some Q implies Θ ` Q :: Γ.
Proof. See fig. 3 and fig. 4 for the most interesting cases. The other cases are similar.
4.2



Progress for cuts

An important property of CP is that all well-typed processes can make communications progress, in the sense that all
top-level cuts can eventually be eliminated by applying reductions and equivalences. In CHOP, we need to be more
careful when studying progress. To see why, consider the following process.
p : (l : 1) ` (νx 1y) (phl = xi | y().z[]) :: z : 1
The process above is well-typed but stuck (cannot progress), because of the free process variable p. In other words, we
lack the code for the left participant in the cut. Notice that here we are not stuck because of incompatible communication
structures between participants, but rather because we still do not know the entirety of the code that we are supposed
to execute.
In general, in CHOP, we may be in a situation where some code is missing. But if we are not missing any code,
then we should not have problems in executing all communications. We call a process open if it has some free process
18

variables, and closed if it has no free process variables. We shall also write that a process P is a cut if its proof ends with
an application of Cut (so P is a restriction term), and that P is a chop if its proof ends with an application of Chop (so
P is an explicit substitution term). Then, CHOP enjoys progress in the sense that any closed process that is a restriction
can be reduced. To prove this, we first establish the following lemma, which states that chops cannot get us stuck.
Lemma 4.2 (Progress for top-level chops). Let Θ ` P :: Γ be a chop. Then, there exists Q such that P −→ Q and
Θ ` Q :: Γ.
Proof. Because of type preservation (theorem 4.1), we only need to find a Q such that P −→ Q.
We proceed by induction on the structure of P. The cases are on the last applied rule for the right premise of the
chop.
If the right premise is itself a chop, we invoke the induction hypothesis and lift the corresponding reduction.
For all other cases, we can either eliminate the top-level chop immediately with a reduction from fig. 5 or push the


chop up the proof with a reduction from fig. 7.
Recall that we write ` P :: Γ when the process environment in the judgement is empty.

Theorem 4.3 (Progress for top-level cuts). Let ` P :: Γ and P be a cut. Then, there exists Q such that P −→ Q and
` Q :: Γ.
Proof. Because of type preservation (theorem 4.1), we only need to find a Q such that P −→ Q.
We now proceed by cases on the last applied rules of the premises of the cut.
If one of the premises is itself a cut, we recursively eliminate it (apply a reduction and lift it to the top-level cut).
If the premises are both applications of rules that act on the channels used in the restriction, then we can apply one
of the reductions in fig. 5. (This may require using an equivalence.)
If one of the premises acts on a channel not named in the restriction, then we apply one of the commuting conversions
in fig. 7.
If one of the premises is a chop, we apply Lemma 4.2 and lift the reduction to the cut.
4.3



General progress and execution strategy

Establishing progress only for top-level cuts is not entirely satisfactory, because it does not give us an execution strategy
for CHOP. What about processes with top-level chops? (Meaning that an explicit substitution is at the top level.) For
example, consider the following term, where ρ = {l 1 = x, l 2 = y, l 3 = z}.
phρi[p:= (ρ) (νx 1y) (x[] | y().z[])]
This process does not have any communications to perform at the top level, so if we just consider top-level cut
elimination we would not execute anything here. However, intuitively we would expect this process to run p by using
the explicit substitution and reduce as follows.
phρi[p:= (ρ) (νx 1y) (x[] | y().z[])] −→−→ z[]
So we need a more general progress result, which considers also chops.
Theorem 4.4 (Progress). Let ` P :: Γ be a cut or a chop. Then, there exists Q such that P −→ Q and ` Q :: Γ.
Proof. Immediate consequence of theorem 4.3 and theorem 4.2.
19



Remark 2. The proof of progress gives us an execution strategy that reaps the benefits of using explicit substitutions.
Consider the following example (we omit the type of the restriction).
(νxy) (x[z].(z[(ρ)P BI G ] | x[inl].P) | y(w).w(p). y.case(Q, R))
This can reduce as follows.
−→−→ (νxy) (x[inl].P | y.case(Q[p:= (ρ)P BI G ], R[p:= (ρ)P BI G ]))
Assume now that P BI G is some big process term, and that both Q and R use variable p. The duplication of the explicit
substitution that we have obtained with the reduction chain is cheap in practice, since we could implement it by using a
shared pointer to a representation of P BI G . This is safe, because the processes inside of explicit substitutions are “frozen”
(cannot be reduced).
However, if we chose to equip CHOP with a semantics that resolves substitutions immediately, as in standard HOπ , we
would put the code of P BI G in both Q and R, leading to a costly duplication. Instead, the execution strategy in the proof of
theorem 4.4 is lazy with respect to substitutions and prefers the following reduction.
−→ (νxy) (P | Q[p:= (ρ)P BI G ])
In the term above, there is no risk of duplicating the code of P BI G unnecessarily anymore.
4.4

Chop elimination

Rule Chop can be seen as a new rule for composing processes, similar to rule Cut, but acting on process variables
instead of connecting channels. Since linear logic supports cut elimination (all cuts can be removed from proofs),
it is natural to ask whether the same can be done for chops. We prove here that CHOP supports chop elimination.
We say that P is chop-free if its proof does not contain any applications of rule Chop. Eliminating all chops from
a proof corresponds to replacing all invocations of a process variable with the body of the process specified by the
corresponding chop that instantiates the variable. This means that CHOP can be seen as a logical reconstruction of
HOπ , where all substitustions are performed immediately after processes are communicated: explicit substitutions just
give an implementation strategy for this mechanism.
We first establish that rule Chop is admissible.
Theorem 4.5 (Chop admissibility). Let Θ ` P :: ∆ρ and Θ 0, p : ∆ ` Q :: Γ, where P and Q are chop-free. Then, there
exists R such that Θ, Θ 0 ` R :: Γ and R is chop-free.
Proof. By induction on the structure of the proof of Θ 0, p : ∆ ` Q :: Γ. We proceed by cases on the last applied rule
in this proof.
If the last applied rule is Id, then Q = phρ 0 i for some ρ 0 , Θ 0 = ·, and Γ = ∆ρ 0 . Then R = P {ρ 0 ◦ ρ −1 } and the thesis
follows (using appropriate α-renaming to avoid clashes between the free names used in ρ 0 and those in P).
For all other cases, we proceed as for the corresponding commuting conversion in fig. 7 (interpreting chop as an
admissible rule) and then invoke the induction hypothesis.
The proof of chop admissibility gives us a methodology for eliminating all chops from proofs.
Theorem 4.6 (Chop elimination). Let Θ ` P :: Γ. Then, there exists Q such that Q is chop-free and Θ ` Q :: Γ.
20



Proof. We iteratively eliminate the inner-most applications of rule Chop in the proof of P, until there are no
more chops. To eliminate these chops, we follow the inductive procedure described in the proof of theorem 4.5, since


inner-most applications have chop-free premises.

5

EXTENSIONS

We illustrate how the basic theory of CHOP can be used to obtain richer features.

5.1

Derivable constructs as syntax sugar

We derive some constructs using the proof theory of CHOP and provide them as syntactic sugar.

Output of free channel names. In CHOP, we can only output bound channel names, as in the internal π -calculus by
Sangiorgi (1996). It is well-known that link terms can be used to simulate the output of a free channel. In CP, this
works, as shown by Lindley and Morris (2015). The same applies to CHOP. We can add the usual term for free channel
output to the syntax of processes.
P, Q, R ::=

···
x hyi.P

output a free channel name and continue

This new term is desugared as follows.
x hyi.P

=

def

x[z].(y → z A

⊥

| P)

The proof of soundness is easy, but reading it is useful to understand the typing of the new construct.
Θ ` P :: Γ, x : B
Θ ` x hyi.P :: Γ, y : A⊥ , x : A ⊗ B

` y → z A :: y : A⊥ , z : A

=

def

Θ ` x[z].(y

⊥
→ zA

Axiom

Θ ` P :: Γ, x : B

| P) :: Γ, y : A⊥ , x : A ⊗ B

⊗

Higher-order I/O with continuations. We can also derive constructs for sending and receiving processes over channels
and then allow us to continue using that channel. We distinguish these sugared counterparts from our output and input
primitives by using bold brackets.
P, Q, R ::=

···
x[(ρ)P].Q

output a process and continue

x(p).P

input a process and continue

These constructs are desugared as follows (we show directly the proofs).
Θ ` P :: ∆ρ Θ 0 ` Q :: Γ, x : A
Θ, Θ 0 ` x[(ρ)P].Q :: Γ, x : [∆] ⊗ A

Θ, p : ∆ ` P :: Γ, x : A
Θ ` x(p).P :: Γ, x : h∆i O A

def

=

Θ ` P :: ∆ρ
[]
Θ ` y[(ρ)P] :: y : [∆]
Θ 0 ` Q :: Γ, x : A
⊗
Θ, Θ 0 ` x[y].(y[(ρ)P] | Q) :: Γ, x : [∆] ⊗ A

=

Θ, p : ∆ ` P :: Γ, x : A
hi
Θ ` y(p).P :: Γ, y : h∆i, x : A
O
Θ ` x(y).y(p).P :: Γ, x : h∆i O A

def

21

Procedures. If the abstraction that we send over a channel does not refer to any free process variable, then we can
always replicate it as many times as we wish. Here is the proof.
` P :: Γρ
[]
` y[(ρ)P] :: y : [Γ]
!
` !x(y).y[(ρ)P] :: x : ![Γ]
We use this property to build a notion of procedures that can be used at will. We denote procedure names with K, for
readability. We will later use it as a channel name in our desugaring.
P, Q, R ::=

···
def K = (ρ)P in Q

procedure definition

K hρi

procedure invocation

A term def K = (ρ)P in Q defines procedure K as (ρ)P in the scope of Q, and a term K hρi invokes procedure K by
passing the parameters ρ.
Here is the desugaring of both constructs. For simplicity of presentation, in term def K = (ρ)P in Q we assume that
K is used at least once in Q. The generalisation to the case where Q does not use K at all is straightforward (thanks to
rule Weaken).

` P :: Γρ Θ ` Q :: Γ, K : ?hΓi
Θ ` def K = (ρ)P in Q :: Γ

=

def

` P :: Γρ
[]
` y[(ρ)P] :: y : [Γ]
!
` !x(y).y[(ρ)P] :: x : ![Γ]
Θ`

=

def

` K hρi :: Γρ, K : ?hΓi

(νx ![Γ] K)

Θ ` Q :: Γ, K : ?hΓi

(!x(y).y[(ρ)P] | Q) :: Γ

Cut

Id
p : Γ ` phρi :: Γρ
hi
` K(p).phρi :: Γρ, K : hΓi
?
` ?K[y].y(p).phρi :: Γρ, K : ?hΓi

Observe that even if procedures can be used at will, typing ensures that each usage respects linearity (i.e., every usage
“consumes” the necessary linear resources available in the context). Note also that self-invocations are not supported, as
typing forbids them.

Higher-order parameters. We chose not to make abstractions parametric on process variables for economy of the
calculus. This feature can be reconstructed with the following syntactic sugar.
P, Q, R ::=

···
xλq.P

named higher-order parameter

P hx = (ρ)Qi

application

The desugaring is simple, interpreting a named higher-order parameter as a channel on which we perform a single
higher-order input.
22

G  (x i : Ai )i , y : C H  Γ, (x i : Bi )i , y : D
⊗O
1⊥
x → y(G).H  Γ, (x i : Ai ⊗ Bi )i , y : C O D
x → y  (x i : 1)i , y : ⊥
G  Γ, x : A, (yi : Ci )i H  Γ, x : B, (yi : D i )i
⊕N
0>
x → y.case(G, H )  Γ, x : A ⊕ B, (yi : Ci N D i )i
x → y.case()  Γ, x : 0, (yi : >)i
G  Γ, x : A, (yi : Bi )i X < ftv(Γ)
G  x : A, (yi : Bi )i
∃∀
?!
!x → y(G)  x : ?A, (yi : !Bi )i
x → y.(X )G  Γ, x : ∃X .A, (yi : ∀X .Bi )i
Axiom
x A → y  x : A, y : A⊥
Fig. 8. CP, Coherence Rules (from (Carbone et al. 2016)).

Θ, p : ∆ ` P :: Γ
Θ ` xλp.P :: Γ, x : h∆i

def

Θ ` Q :: ∆ρ Θ 0 ` P :: Γ, x : h∆i
Θ, Θ 0 ` P hx = (ρ)Qi :: Γ

def

=

Θ, p : ∆ ` P :: Γ
hi
Θ ` x(p).P :: Γ, x : h∆i

=

Θ ` Q :: ∆ρ
[]
Θ ` y[(ρ)Q] :: y : [∆]
Θ, Θ 0

`

Θ 0 ` P :: Γ, x : h∆i

(νy [∆]x)

:: Γ

Cut

Notice that the desugaring of P hx = (ρ)Qi yields a process that allows for reductions to happen in P before the
application takes place, since the corresponding higher-order named parameter term may be nested inside of P. Also,
this desugaring cannot be implemented by merely using an application of rule Chop, since p is bound to P in term
xλp.P (as can be observed by its desugaring), and Chop acts on free process variables.

5.2

Multiparty sessions

In (Carbone et al. 2016, 2017b), CP was extended to support multiparty sessions, yielding a logical reconstruction of the
theory of multiparty session types by Honda et al. (2016). Multiparty session types allow for typing sessions with more
than two participants. A discussion of their usefulness goes beyond the scope of this paper. The interested reader may
consult (Ancona et al. 2016). What we are interested in here is to illustrate how CHOP can support multiparty sessions.
The key to having multiparty sessions is to change the Cut rule to the following CCut rule. We adapt the version
from (Carbone et al. 2016) to our higher-order contexts. We write x A as an abbreviation of x 1A1 , . . . , x nAn (likewise for P,
Γ).

(Θi ` Pi :: Γi , x i : Ai )i

G  (x i : Ai )i

CCut

(νx A : G) (P) ` Γ
The differences between Cut and the new CCut (for Coherence Cut) are: we are now composing in parallel an
unbounded number of processes Pi , each one implementing type Ai at the respective channel x i ; and, we use a new
coherence judgement G  (x i : Ai )i to check the compatibility of these types. The type G in the coherence judgement
(and the restriction term) is a global type that prescribes how all participants in the session should communicate. The
rules for deriving these judgements for CP are displayed in fig. 8. Coherence rules check that the types of participants
can be matched accordingly to the global type, which is interpreted as a proof term.
23

Extending coherence to CHOP is straightforward, as we just need to add a rule for our new type constructors
regarding process mobility. Here is the rule.
x → y(∆)  x : [∆], y : h∆i

[]hi

And this is the principal reduction for process communication in the multiparty system.
(νx [∆]y h∆i : x → y(∆)) (x[(ρ)P] | y(p).Q) −→ Q[p:= (ρ)P]
Deriving the other reductions and equivalences for CHOP with multiparty communications is a straightforward exercise
in adapting the rules from (Carbone et al. 2016).
Following the same idea used for building syntax sugar for process output with continuation at the end of section 5.1,
we could also develop syntax sugar for global types that allows for continuations after process communications, or
even multicasts of process terms, by using auxiliary channel communications.

6

FROM CHOP TO CP

The original presentation of the π -calculus by Milner et al. (1992) does not include process mobility, only channel
mobility. This was motivated by the belief that channel mobility can be used to simulate the effects obtained by using
process mobility. Sangiorgi (1993) later proved this belief to be correct, by showing a fully-abstract encoding from HOπ
to the π -calculus. In this section, we show that a translation can be developed also from CHOP to CP. Namely, process
terms in CHOP, which may use process mobility, can be translated to terms in CP, which may not. We show that the
translation supports type preservation and an operational correspondence.
The latest version of the calculus CP, from (Carbone et al. 2016), is equivalent to a fragment of CHOP. Formally, for
this section, let CP be the calculus obtained from fig. 2 by removing the rules Id, [], hi, and Chop (the process mobility
rules), and also by removing process contexts (Θ) from all other rules.
We now define a translation JPK from processes P in CHOP to CP. The key idea for the translation is that the

output of a process–x[(ρ)P]—is translated to sending a reference (a channel) to an instance of P, guarded by a series
of inputs to receive the formal parameters (ρ). Dually, the input of a process receives such reference. Finally, the
invocation of a process variable is translated to a series of outputs which provide the actual parameters. Without
loss of generality, we assume that there is an unused set of channels in P indexed by process variables, i.e., the set of
channels {x p | p is a process variable}. Intuitively, x p is the channel used to encode the behaviour of the process stored
in variable p.
The main rules that define the translation are given in fig. 9, and follow the reasoning described above. All the other
rules are displayed in fig. 10. In the rules, we abuse notation and define the translation as taking proof trees in CHOP to
process terms in CP. (Similarly to the presentation of the translation of functional programs in the calculus GV into CP
by Wadler (2014).) This eliminates ambiguity on the distribution and usage of names, types, and environments. We also
represent parameter records ρ as ordered according to lexicographic ordering on labels.
The translation makes use of a type translation JAK from types in CHOP to types in CP, since CP does not have the

types [∆] and h∆i. The type translation is defined in fig. 11.

The translation JPK preserves types, up to usages of process variables, which are translated to usages of the

corresponding channels that implement these variables. To state this formally, we need to translate types of process
24

s

Θ ` P :: ∆ρ Θ 0, p : ∆ ` Q :: Γ
Chop
Θ, Θ 0 ` Q[p:= (ρ)P] :: Γ

{

= (νx p J∆K yp ) JQK | yp (z 1 ). · · · .yp (zk ).yp (). JPK

Id

z

= x p hz 1 i. · · · .x p hzk i.x p []

Θ ` P :: Γρ
[]
Θ ` x[(ρ)P] :: x : [Γ]

{

Θ, p : ∆ ` Q :: Γ
hi
Θ ` x(p).Q :: Γ, x : h∆i

{

r
s
s

p : Γ ` phρi :: Γρ

= x[y]. y(z 1 ). · · · .y(zk ).y(). JPK | x[]



where ρ = {l = z}
where ρ = {l = z}



where ρ = {l = z}

= x(x p ).x(). JQK

Fig. 9. Translating CHOP to CP, Rules for Process Mobility.

variables into channel types as follows.
J·K

JΘ, p : ∆K

=

·

=

JΘK , x p : J∆K

Theorem 6.1. Let Θ ` P :: Γ in CHOP. Then, ` JPK :: JΘK , JΓK in CP.
Proof. By induction on the structure of P. For the proof cases, just apply the typing rules of CP by following the
structure of the process terms on the right of the translation rules.



Notice how the process variables that a process depends on in CHOP become extra channels that the translation
needs in CP (JΘK), as expected. Of course, if the original CHOP process does not depend on any free process variables,
then the result of the translation does not depend on any such extra channels, as formalised by the following corollary.
Corollary 6.2. Let ` P :: Γ in CHOP. Then, ` JPK :: JΓK in CP.
Let −→∗ be the transitive closure of −→ and −→+ be defined as −→∗ −→. The translation supports the following
operational correspondence.
Theorem 6.3. Θ ` P :: Γ implies the following properties.
• (Completeness) If P → P 0 , then JPK −→+ JP 0 K.

• (Soundness) If JPK −→∗ Q, then P −→+ P 0 for some P 0 such that Q −→∗ JP 0 K.
7

RELATED WORK

Since its inception, linear logic was described as the logic of concurrency (Girard 1987). Correspondences between the
proof theory of linear logic and variants of the π -calculus emerged soon afterwards (Abramsky 1994; Bellin and Scott
1994), by interpreting linear logic propositions as types for channels. Later, linearity inspired also the seminal theories
of linear types for the π -calculus (Kobayashi et al. 1999) and session types (Honda et al. 1998). Even though the two
theories do not use exactly linear logic, the work by Dardha et al. (2017) shows that the link is still strong enough that
session types can be encoded into linear types.
It took more than ten years for a formal correspondence between linear logic and (a variant of) session types to
emerge, with the seminal paper by Caires and Pfenning (2010). This then inspired the development of Classical Processes
25

r
t

` x → y A :: x : A⊥ , y : A

Θ ` P :: Γ, x : A

Cut

Θ ` P :: Γ, y : A Θ 0 ` Q :: ∆, x : B
⊗
Θ, Θ 0 ` x[y].(P | Q) :: Γ, ∆, x : A ⊗ B
Θ ` P :: Γ, y : A, x : B
O
Θ ` x(y).P :: Γ, x : A O B

s
s

Θ ` P :: Γ, x : A
⊕1
Θ ` x[inl].P :: Γ, x : A ⊕ B
s
s

{

Θ ` P :: Γ, y : A
?
Θ ` ?x[y].P :: Γ, x : ?A

r

= ?x[y]. JPK

= x(y). JPK

s

{

{

= x[JAK]. JPK

` P :: ?Γ, y : A
!
` !x(y).P :: ?Γ, x : !A

s

Θ ` x[] :: x : 1
r

1

z

= x[]

s

{

>

z

= !x(y). JPK

{

= JP {x/y, x/z}K
{

= x(). JPK

= x .case()

Fig. 10. Translating CHOP to CP, Other Rules.

J[∆]K
Jh∆iK
J(li : Ai )i K

=
=
=


J∆K ⊥ ⊗ 1
J∆K O
q
y ⊥
q ⊥y
A⊥
1 ⊗ · · · ⊗ An

JA ⊗ BK = JAK ⊗ JBK JA O BK = JAK O JBK
JA ⊕ BK = JAK ⊕ JBK JA N BK = JAK N JBK
J0K = 0 J>K = > J1K = 1 J⊥K = ⊥ JX K = X
J?AK = ? JAK J!AK = ! JAK J∃X .AK = ∃X . JAK J∀X .AK = ∀X . JAK
Fig. 11. Translation of types from CHOP to CP.

26

= x[inr]. JPK

= x(X ). JPK

Θ ` P :: Γ
⊥
Θ ` x().P :: Γ, x : ⊥

Θ ` x .case() :: Γ, x : >

{

Θ ` P :: Γ
Weaken
Θ ` P :: Γ, x : ?A

Θ ` P :: Γ, y : ?A, z : ?A
Contract
Θ ` P {x/y, x/z} :: Γ, x : ?A

{

= x .case(JPK , JQK)

Θ ` P :: Γ, x : B X < ftv(Θ) ∪ ftv(Γ)
∀
Θ ` x(X ).P :: Γ, x : ∀X .B

Θ ` P :: Γ, x : B{A/X }
∃
Θ ` x[A].P :: Γ, x : ∃X .B
s

{

= x[y].(JPK | JQK)

Θ ` P :: Γ, x : B
⊕2
Θ ` x[inr].P :: Γ, x : A ⊕ B

s

= x[inl]. JPK

= x → y JAK

= (νx JAK y) (JPK | JQK)

{

{

Θ ` P :: Γ, x : A Θ ` Q :: Γ, x : B
N
Θ ` x .case(P, Q) :: Γ, x : A N B

s
s

|

Θ 0 ` Q :: ∆, y : A⊥

Θ, Θ 0 ` (νx Ay) (P | Q) :: Γ, ∆
s

z

Axiom

{

= JPK

(CP) by Wadler (2014), which we have already discussed plentifully in this article. We have extended this line of work
to include process mobility. Process mobility has been studied deeply in the context of the π -calculus, starting from the
inception of the Higher-Order π -calculus (HOπ ) by Sangiorgi (1993). The definition of HOπ does not require a typing
discipline. Differently, the definition of CHOP is based on a typing discipline that treats process variables linearly. Also,
our semantics is not defined a-priori as in most calculi, but rather derived by sound proof transformations allowed by
our proof theory. The proof theory of CHOP generalises linear logic by allowing to assume that some judgements can
be proven, and to provide evidence for resolving these assumptions. Similar ideas have been used in the past in different
contexts, for example for modal logic (Nanevski et al. 2008) and logical frameworks (Bock and Schürmann 2015).
The concept of explicit substitution has been originally introduced to formalise execution strategies for the λ-calculus
that are more amenable to efficient implementations (Abadi et al. 1991). The proof theory of CHOP naturally yields a
theory of explicit substitutions for higher-order processes. (Sangiorgi 1993) used a similar syntax as syntactic sugar; its
desugaring is similar to that of our procedures in section 5.
The first version of multiparty session types is discussed in detail in (Honda et al. 2016). Multiparty session types
is currently a popular research topic, and there is a substantial body of work on multiparty sessions. Our multiparty
version of CHOP in section 5.2 is the first that introduces process mobility to this line of work, and illustrates how typing
can be used to guarantee progress in this setting. The first formulation of how multiparty sessions may be supported in
the setting of linear logic (without process mobility) was given in (Carbone et al. 2015), and later investigated further
in (Carbone et al. 2017b) and in (Carbone et al. 2016).
Other session calculi include primitives for moving processes by relying on a functional layer (Mostrous and Yoshida
2015; Toninho et al. 2013). Differently, CHOP offers the first logical reconstruction of (a linear variant of) HOπ (Sangiorgi
1993), where mobile code is just processes, instead of functions (or values as intended in λ-calculus). The key difference
with (Toninho et al. 2013) is that CHOP treats process variables linearly. Of course, process abstractions and functions
can be seen as equivalent ideas. We chose the abstraction formulation because it allows us to use CLL contexts as
higher-order types directly, making the theory of CHOP simpler. For example, we do not require the additional
asymmetric connectives in session types used in (Toninho et al. 2013) for communicating processes (τ ⊃ A and τ ∧ A).
The “send a process and continue over channel x” primitive found in (Mostrous and Yoshida 2015; Toninho et al.
2013) can be encoded in CHOP, as shown in section 5.1. Since process variables are non-linear functional values in
(Toninho et al. 2013), the usage of process variables does not follow a discipline of linearity as in CHOP, offering less
control. However, the functional layer in (Toninho et al. 2013) allows for a remarkably elegant integration of recursive
types, which we left out of the scope of this article. A potential direction to recover this feature is the work presented
in (Toninho et al. 2014). Our notion of explicit substitution for higher-order processes is new, and may be adopted also
in the settings of (Toninho et al. 2013) and (Mostrous and Yoshida 2015) for devising efficient execution strategies. The
work in (Toninho et al. 2013) also has a logical basis, like ours. CHOP has the advantage of being formulated as an
extension of classical linear logic, in a way that integrates well with existing features. This allows us, for example,
to achieve multiparty sessions, which at this time is still unclear how to do in the intuitionistic setting of (Toninho
et al. 2013). No encoding of higher-order processes to first-order processes is provided in (Mostrous and Yoshida 2015;
Toninho et al. 2013).
The calculus of Linear Compositional Choreographies (LCC) (Carbone et al. 2017a) gives a propositions as types
correspondence for Choreographic Programming (Montesi 2013) based on linear logic. CHOP may provide the basis for
extending LCC with process mobility, potentially yielding the first higher-order choreography calculus.
27

Atkey (2017) investigated a notion of observational equivalence for CP and a denotational semantics to capture it.
His formulation requires the introduction of additional syntax and typing rules, in order to define parallel compositions
that leave the names of connected channels free and include processes with empty behaviour (Mix0 ). Thus, we left an
investigation of observational equivalence for CHOP to future work, which would require extending Atkey’s work to
our higher-order constructs. We conjecture that extending the denotational semantics defined by Atkey can benefit from
our translation of higher-order types as channel types. An immediate application would be to prove a full abstraction
result for our translation from CHOP to CP—this would not be very surprising, given the structure of our translation,
and also because the denotational semantics of higher-order types would probably be defined similarly to our type
translation.

8

CONCLUSIONS

We presented the calculus of Classical Higher-Order Processes (CHOP), an extension of Classical Processes (CP) (Wadler
2014) to mobile code. Our formulation extends Classical Linear Logic (CLL) to higher-order reasoning, viewing proofs
as linear “resources” that can be used to assume premises in other proofs. CHOP integrates well with the existing
features of linear logic, as we illustrated in sections 3 and 5.
The translation from CHOP to CP shows how our higher-order processes that use mobile code can be simulated
by using reference passing instead. This result is distinct from the original one by Sangiorgi (1993), because we
are operating in a typed setting. Understanding what a calculus with behavioural types, such as session types, can
express—i.e., what well-typed terms can model—is a nontrivial challenge in general (Pérez 2016). Our translation shows
that the proof theory of CP is powerful enough to simulate higher-order processes in the proof theory of CHOP. In
practice, this has the usual implications: the translation gives us the possibility to write programs that use code mobility
andthen choose later whether we should really use code mobility or translate it to an implementation basedon reference
passing. This choice depends on the application case. If we are modelling the transmission of an application to be run
somewhere else (as in cloud computing), then code mobility is necessary. Otherwise, if we are in a situation where
we can choose freely, then we should choose whichever implementation is more efficient. For example, code mobility
is useful if two processes, say a client and a server, are operating on a slow connection; then, instead of performing
many communications over the slow connection, the client may send an application to the server such that the server
can communicate with the application locally, and then send to the client only the final result. Lastly, if we are using
code mobility in an environment where communications are implemented in local memory (as in many object-oriented
language implementations or other emerging languages, like Go), then the translation gives us a compilation technique
towards a simpler language without code mobility (CP), which we can use to simplify runtime implementations.
Process mobility is the underlying concept behind the emerging interest on runtime adaptation, a mechanism by
which processes can receive updates to their internal code at runtime. Different attempts at formalising programming
disciplines for runtime adaptations have been made, e.g., by Bono et al. (2017); Dalla Preda et al. (2017); Di Giusto
and Pérez (2015), but none are rooted in a propositions as types correspondence and all offer different features and
properties. CHOP brings us one step nearer to formulating adaptable processes based on the firm foundations of linear
logic.

ACKNOWLEDGMENTS
The author thanks Luı́s Cruz-Filipe, Marco Peressotti, and Davide Sangiorgi for useful discussions.
28

REFERENCES
Martı́n Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy. 1991. Explicit Substitutions. J. Funct. Program. 1, 4 (1991), 375–416.
Samson Abramsky. 1994. Proofs as Processes. Theor. Comput. Sci. 135, 1 (1994), 5–9.
Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Deniélou, Simon J. Gay, Nils Gesbert, Elena Giachino,
Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T.
Vasconcelos, and Nobuko Yoshida. 2016. Behavioral Types in Programming Languages. Foundations and Trends in Programming Languages 3, 2-3
(2016), 95–230. https://doi.org/10.1561/2500000031
Robert Atkey. 2017. Observed Communication Semantics for Classical Processes. In ESOP (Lecture Notes in Computer Science), Vol. 10201. Springer, 56–82.
Gianluigi Bellin and Philip J. Scott. 1994. On the pi-Calculus and Linear Logic. TCS 135, 1 (1994), 11–65.
Peter Brottveit Bock and Carsten Schürmann. 2015. A Contextual Logical Framework. In LPAR (Lecture Notes in Computer Science), Vol. 9450. Springer,
402–417.
Viviana Bono, Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. 2017. Data-driven adaptation for smart sessions. J. Log. Algebr. Meth.
Program. 90 (2017), 31–49.
Luı́s Caires and Frank Pfenning. 2010. Session Types as Intuitionistic Linear Propositions. In CONCUR. 222–236.
Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Schürmann, and Philip Wadler. 2016. Coherence Generalises Duality: A Logical Explanation of
Multiparty Session Types. In CONCUR (LIPIcs), Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 33:1–33:15.
Marco Carbone, Fabrizio Montesi, and Carsten Schürmann. 2017a. Choreographies, logically. Distributed Computing (2017), 1–17. https://doi.org/10.1007/
s00446-017-0295-1 Also: CONCUR, pages 47–62, 2014.
Marco Carbone, Fabrizio Montesi, Carsten Schürmann, and Nobuko Yoshida. 2015. Multiparty Session Types as Coherence Proofs. In CONCUR. 412–426.
Marco Carbone, Fabrizio Montesi, Carsten Schürmann, and Nobuko Yoshida. 2017b. Multiparty session types as coherence proofs. Acta Informatica
(2017). https://doi.org/10.1007/s00236-016-0285-y
Mila Dalla Preda, Maurizio Gabbrielli, Saverio Giallorenzo, Ivan Lanese, and Jacopo Mauro. 2017. Dynamic Choreographies: Theory And Implementation.
Logical Methods in Computer Science 13, 2 (2017).
Ornela Dardha, Elena Giachino, and Davide Sangiorgi. 2017. Session types revisited. Inf. Comput. 256 (2017), 253–286.
Cinzia Di Giusto and Jorge A. Pérez. 2015. Disciplined structured communications with disciplined runtime adaptation. Sci. Comput. Program. 97 (2015),
235–265.
Jean-Yves Girard. 1987. Linear Logic. Theor. Comput. Sci. 50 (1987), 1–102. https://doi.org/10.1016/0304-3975(87)90045-4
Kohei Honda, Vasco Vasconcelos, and Makoto Kubo. 1998. Language primitives and type disciplines for structured communication-based programming.
In ESOP. 22–138.
Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2016. Multiparty Asynchronous Session Types. JACM 63, 1 (2016), 9. Also: POPL, 2008, pages
273–284.
Naoki Kobayashi, Benjamin C. Pierce, and David N. Turner. 1999. Linearity and the pi-calculus. ACM Trans. Program. Lang. Syst. 21, 5 (1999), 914–947.
https://doi.org/10.1145/330249.330251
Sam Lindley and J. Garrett Morris. 2015. A Semantics for Propositions as Sessions. In ESOP (Lecture Notes in Computer Science), Vol. 9032. Springer,
560–584.
Robin Milner, Joachim Parrow, and David Walker. 1992. A Calculus of Mobile Processes, I. Inf. Comput. 100, 1 (1992), 1–40.
Fabrizio Montesi. 2013. Choreographic Programming. Ph.D. Thesis. IT University of Copenhagen. http://www.fabriziomontesi.com/files/choreographic
programming.pdf.
Fabrizio Montesi. 2017. Classical Higher-Order Processes - (Short Paper). In FORTE (Lecture Notes in Computer Science), Vol. 10321. Springer, 171–178.
Dimitris Mostrous and Nobuko Yoshida. 2015. Session typing and asynchronous subtyping for the higher-order π -calculus. Inf. Comput. 241 (2015),
227–263.
Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. 2008. Contextual modal type theory. ACM Trans. Comput. Log. 9, 3 (2008), 23:1–23:49.
Jorge A. Pérez. 2016. The Challenge of Typed Expressiveness in Concurrency. In FORTE (Lecture Notes in Computer Science), Vol. 9688. Springer, 239–247.
Davide Sangiorgi. 1993. From pi-Calculus to Higher-Order pi-Calculus - and Back. In TAPSOFT (Lecture Notes in Computer Science), Vol. 668. Springer,
151–166.
Davide Sangiorgi. 1996. Pi-Calculus, Internal Mobility, and Agent-Passing Calculi. TCS 167, 1&2 (1996), 235–274.
Davide Sangiorgi and David Walker. 2001. The Pi-Calculus - a theory of mobile processes. Cambridge University Press.
Bernardo Toninho, Luı́s Caires, and Frank Pfenning. 2013. Higher-Order Processes, Functions, and Sessions: A Monadic Integration. In ESOP (Lecture
Notes in Computer Science), Vol. 7792. Springer, 350–369.
Bernardo Toninho, Luı́s Caires, and Frank Pfenning. 2014. Corecursion and Non-divergence in Session-Typed Processes. In TGC (Lecture Notes in Computer
Science), Vol. 8902. Springer, 159–175.
Philip Wadler. 2014. Propositions as sessions. JFP 24, 2–3 (2014), 384–418. Also: ICFP, pages 273–286, 2012.
Christopher P Wadsworth. 1971. Semantics and Pragmatics of the Lambda-Calculus. Ph.D. Dissertation. University of Oxford.

29

