# Classical Higher-Order Processes

Fabrizio Montesi

► To cite this version:

Fabrizio Montesi. Classical Higher-Order Processes. 37th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2017, Neuchâtel, Switzerland. pp.171-178, 10.1007/978-3-319-60225-7_12. hal-01658427

HAL Id: hal-01658427

https://inria.hal.science/hal-01658427

Submitted on 7 Dec 2017

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Classical Higher-order Processes
(Short Paper)

Fabrizio Montesi

University of Southern Denmark

**Abstract.** Classical Processes (CP) is a calculus where the proof theory of classical linear logic types processes à la π-calculus, building on a Curry-Howard correspondence between session types and linear propositions. We contribute to this research line by extending CP with process mobility, inspired by the Higher-Order π-calculus. The key to our calculus is that sequents are asymmetric: one side types sessions as in CP and the other types process variables, which can be instantiated with process values. The controlled interaction between the two sides ensures that process variables can be used at will, but always respecting the linear usage of sessions expected by the environment.

# 1 Introduction

Session types define protocols that discipline how concurrent processes may interact [?]. The type theory of sessions for (a variant of) the π-calculus [?] was found to be in a Curry-Howard correspondence with intuitionistic linear logic, where processes correspond to proofs, session types to propositions, and communication to cut elimination [?]. Properties that are normally obtained through additional machinery on top of session types, like deadlock-freedom, come for free from the properties of linear logic, like cut elimination. The correspondence was later revisited for classical linear logic, yielding the calculus of Classical Processes (CP) [?]. The design of CP is guided by the logic, making the correspondence stricter at the cost of deviating some more from the standard π-calculus.

The solidity of the correspondence between session types and linear logic propositions has been confirmed repeatedly. From the initial seminal idea, different extensions have been proposed in order to capture, among others, multiparty sessions [?,?], the paradigm of choreographic programming [?,?], behavioural polymorphism [?,?,?,?], and integrations with functional programming [?].

In this paper, we begin extending this research line towards a key generalisation of the π-calculus: the Higher-Order π-calculus (HOπ) [?]. HOπ supports process mobility: communicated values can be processes, which can then be run or re-transmitted by the receiver – by using *process variables* to refer to the received processes in its program. Our main contribution is the development of CHOP (Classical Higher-Order Processes), which extends CP to process mobility in the same fashion as in HOπ. In CP, typing judgements are of the form $P \vdash \Delta$, read “process *P* uses its sessions according to *Δ*”. If we ignore the *P*, this is the
standard one-sided sequent form of classical linear logic. The key aspect of CHOP is that it extends the one-sided sequents used in CP to two-sided sequents, which are manipulated by combining the typing of linear channels of CP (on the right) with a new discipline that types process variables (on the left). So our typing judgements are now of the form $\Theta \vdash P :: \Delta$, read "process P uses its session endpoints according to $\Delta$, possibly using some process variables according to $\Theta$". Why the "possibly" for the usage of process variables? In $HO\pi$, a process variable can be used by the receiving process at will (zero or more times). This expressivity is carried over to CHOP by interpreting process variables as non-linear resources. As a result, we get a hybrid type system that consists of two fragments. The first is inherited directly from CP, used to manipulate linear resources (session communications), while the second disciplines the usage of process variables.

## 2 Classical Higher-Order Processes (CHOP)

We introduce the calculus of Classical Higher-Order Processes (CHOP), which extends the latest version of the calculus of Classical Processes (CP) [?].

*Types* There are two kinds of types in CHOP: session types, ranged over by $A, B, C, D$, and process types, ranged over by $T$. Session types are inherited directly from CP, and correspond to linear logic propositions. We range over atomic propositions in session types with $X, Y$. Process types are used to type the communication of processes and the use of process variables.

We start by giving the syntax of session types, in the following, along with a short explanation of their meanings.

<table><thead><tr><th colspan="2">A, B, C, D ::=</th><th></th><th></th></tr></thead><tbody><tr><td>A</td><td>⊗</td><td>B</td><td>(send A, proceed as B)</td></tr><tr><td>A</td><td>⊕</td><td>B</td><td>(select A or B)</td></tr><tr><td></td><td>0</td><td>(unit for ⊕)</td><td>A ⊗ B</td><td>(receive A, proceed as B)</td></tr><tr><td></td><td>1</td><td>(unit for ⊗)</td><td>A &amp; B</td><td>(offer A or B)</td></tr><tr><td></td><td>?</td><td>A</td><td>⊤</td><td>(unit for &amp;)</td></tr><tr><td></td><td>∃</td><td>X.A</td><td>⊥</td><td>(unit for ⊗)</td></tr><tr><td></td><td></td><td>(client request)</td><td>!A</td><td>(server accept)</td></tr><tr><td></td><td></td><td>(existential)</td><td>∀X.A</td><td>(universal)</td></tr><tr><td></td><td></td><td>(atomic propositions)</td><td>X<sup>⊥</sup></td><td>(dual of atomic proposition)</td></tr></tbody></table>

CP uses the standard notion of duality from linear logic to check that types are compatible. Above, each type constructor on the left-hand side is dual to that used on the right-hand side. We write $A^{\perp}$ for the type dual to $A$, defined inductively in the standard way (cf. [?] for details). For example, $(A \otimes B)^{\perp} = A^{\perp} \otimes B^{\perp}$.

Each session in CP has two endpoints (one for each process in the session). Endpoints are ranged over by $x, y, z$. Session environments, ranged over by $\Gamma, \Delta$, associate endpoints to session types: $\Gamma = \{x_1 : A_1, \dots, x_n : A_n\}$. We make the standard assumption that $\Gamma$ and $\Delta$ have distinct endpoints when writing $\Gamma, \Delta$.

In CHOP, we can refer to processes that we receive at runtime (via process mobility) by using process variables, ranged over by $p, q, r$. A process environment $\Theta$ maps process variables to process types: $\Theta = \{p_1 : T_1, \dots, p_n : T_n\}$. There is only one form for process types: $T ::= \Theta \rightarrow \Delta$. A process type assignment
<figure><img src="image_2.png" /><figcaption>**Fig. 1.** CHOP, Selected Typing Rules (Part 1, Sessions).</figcaption></figure>

$p: \Theta \rightarrow \Delta$ reads "p implements $\Delta$ provided that the process variables in $\Theta$ are available". Note that $\Theta$ may be empty, meaning that $p$ does not need to invoke other process variables to implement its session behaviour as specified in $\Delta$.

*Processes and Typing* Let $P, Q, R$ range over processes, the program terms of CHOP. We explain terms together with their respective typing rules. A typing judgement $\Theta \vdash P :: \Delta$ states that $P$ implements the communication behaviour specified in $\Delta$, possibly using the process variables specified in $\Theta$.

We first briefly recap the terms and typing rules that we inherit from CP, displayed in Figure ??.. (We omit the rules for exponentials and quantifiers, for space reasons. $\Theta$ is carried in the same way as for the other rules.) The process terms in Figure ?? are the same as in [?]. We adopt the same convention of having sent objects always in square brackets [...] , and, dually, in an input operation the received variable is always bound in round parentheses (...). The endpoint name that we output in a send $x[y]$.($P$ | $Q$) and in a client request ?$x[y]$. $P$ is bound, as in the internal $\pi$-calculus [?]. (This will not be the case for process variables, as we are going to see shortly.) A forwarder term $x \rightarrow y^B$ forwards communications from $x$ to $y$. The restriction term $(\nu x^A y)(P | Q)$ connects two endpoints $x$ and $y$ to form a session, thus $x$ and $y$ are now able to communicate.

We now move to the new terms and typing rules introduced in this work for the communication of process terms, given in Figure ??.

Rule MP allows us to use process variables. It states that if we invoke a process variable $p$, typed with $\Theta \rightarrow \Delta$, and the process environment provides all the process variables that $p$ may in turn use according to $\Theta$, then we obtain an implementation of the session behaviour specified by $\Delta$.

There are two ways of instantiating a process variable. One is receiving a process $-x(p).R$ - which allows us to use $p$ later on (Rule $\vdash R$). The other is by defining the body of a variable explicitly. We denote this as an *explicit substitution*
$$ \begin{array}{ccc} \overline{\Theta', \Theta, p : \Theta \to \Delta \vdash p :: \Delta} & \text{MP} & \frac{\Theta' \vdash Q :: \Delta' \quad \Theta, q : \Theta' \to \Delta' \vdash P :: \Delta}{\Theta \vdash P[q:=Q] :: \Delta} \quad \text{CHOP} \\ \hline \\ \frac{\Theta \vdash P :: \Delta}{\Theta \vdash x[P] :: x : \Theta \to \Delta} \to R & & \frac{\Theta, p : T \vdash R :: \Delta}{\Theta \vdash x(p).R :: \Delta, x : T^{\perp}} \perp R \end{array} $$

<caption>**Fig. 2.** CHOP, Typing Rules (Part 2, Higher-Order Processes).</caption>

(inspired by the $\lambda\sigma$-calculus [?]) $P[q:=Q]$, read “let $q$ be $Q$ in $P$”. We formalise how substitutions are propagated and applied later on, in our semantics for CHOP. Rule CHOP allows us to substitute $Q$ for $q$ in $P$, provided that $Q$ and $q$ have compatible typing. 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$. This idea is also the reason for which Modus Ponens (MP), which is usually admissible, is given as an axiom. Since $p$ represents a missing part of our proof, we do not know that its type is valid (i.e., that there exists a proof for some $P$ such that $\Theta \vdash P :: \Delta$). We delegate this responsibility to the term that instantiates $p$ with a process.

Lastly, a term $x[P]$ sends $P$ along $x$ (recalling a weakened version of the right rule for implication, $\to R$).

As an example, consider the following cloud server implementation. It provides a choice between two options. In the first case, we expect the client to send us an application $p$ to run, which requires a connection with an internally-provided database ($DB$). In the second case, we expect to receive both the application $p$ and the database $q$ that it needs to use, putting them in parallel. (Thus, we may decide to use $DB$ or not.) We omit the types for restrictions.

$$ ( \mathit{xcase}( \mathit{x}(p).(\nu zw)(p \mid d), \mathit{x}(y).\mathit{x}(p).\mathit{y}(q).(\nu zw)(p \mid q) ) ) [d:=DB] $$

*Semantics* To give a semantics to CHOP, we follow the same approach as in [?,?]: we derive term reductions and equivalences from sound proof transformations.

Communications in CHOP are still defined by cut reductions over linear propositions, as in CP. The key insight that underlies our semantics for process mobility is that we interpret process types as atomic propositions in linear logic. That is, in the eyes of linear logic, a process type $T$ is an atomic proposition ($X$). This twist allows us to integrate the expressivity of CP with our new rules: the dual of $T$ is just $T^{\perp}$. (Different typing systems are often integrated this way.) A consequence is that we can cut a process output with a process input, as below.

$$ \frac{\frac{\Theta \vdash P :: \Delta}{\Theta \vdash x[P] :: x : \Theta \to \Delta} \to R \qquad \frac{\Theta, p : \Theta \to \Delta \vdash Q :: \Gamma}{\Theta \vdash y(p).Q :: \Gamma, y : (\Theta \to \Delta)^{\perp}} \perp R}{\Theta \vdash (\nu x^{\Theta \to \Delta} y)(x[P] \mid y(p).Q) :: \Gamma} \quad \text{CUT} $$
The above cut can always be eliminated by rewriting it into a (smaller) chop:

$$ \frac{\Theta \vdash P :: \Delta \quad \Theta, p : \Theta \to \Delta \vdash Q :: \Gamma \qquad \text{CHOP}}{\Theta \vdash Q[p := P] :: \Gamma} $$

By following this idea we can derive the key β-reductions (—>) for process mobility in CHOP, given in the following. We also give some examples of equivalences (≡) that define how explicit substitutions are propagated.

$$ \begin{align*} (\nu x^{\Theta \to \Delta} y) (x[P] \mid y(p).Q) &\to Q[p := P] \\ p[p := P] &\to P \\ (x[y].(Q \mid R))[p := P] &\equiv x[y].(Q[p := P] \mid R[p := P])) \\ (x(y).Q)[p := P] &\equiv x(y).(Q[p := P]) \end{align*} $$

For space reasons, we do not include all reductions and conversions. Note that we inherit all the original ones from CP (cf. [?]), for example those given below.

$$ \begin{align*} (\nu x^A y) (w \to x^A \mid Q) &\to Q\{w/y\} \\ (\nu x^{A \otimes B} y) (x[u].(P \mid Q) \mid y(v).R) &\to (\nu u^A v) (P \mid (\nu x^B y) (Q \mid R)) \\ (\nu x^1 y) (x[] \mid y().P) &\to P \\ (\nu x^{A \oplus B} y) (x[inl].P \mid y.\text{case}(Q, R)) &\to (\nu x^A y) (P \mid Q) \\ (\nu x^{A \oplus B} y) (x[inr].P \mid y.\text{case}(Q, R)) &\to (\nu x^B y) (P \mid R) \\ (\nu x^{\exists X.B} y) (x[A].P \mid y(X).Q) &\to (\nu x^{B\{A/X\}} y) (P \mid Q\{A/X\}) \end{align*} $$

# 3 Related Work

Other session calculi include primitives for moving processes by relying on a functional layer [?,?]. Differently, CHOP is nearer to the original Higher-Order π-calculus (HOπ) [?], where the communicated values are processes, instead of functions (or values as intended in λ-calculus). A consequence is that the theory of CHOP is simpler. For example, our language of session types remains separate from process types, which are opaque atomic propositions in the session types of CHOP. As such, we do not require the additional asymmetric connectives in session types used in [?] for communicating processes (⊃ and ∧). The “send a process and continue over channel x” primitive of [?] can be encoded in CHOP as $x[y].(y[P] \mid Q)$ (similarly for receive). However, the functional layer in [?] allows for a remarkably elegant integration of recursive types, which is missing in CHOP. A possible direction to recover this feature is the work presented in [?].

In previous works, the process values that can be sent usually have the form $\lambda\tilde{x}.P$, to enable reuse in contexts that use different channel names. In CHOP, this is not necessary since we can get the same result with the forwarder term inherited from CP, which the receiver of a process can use to manipulate its names. For example, suppose that $p$ has a free session endpoint $x$ that we want to rename to $w$. We can just write $(\nu y^A x) (w \to y^A \mid p)$ to obtain the desired
effect: whichever process will replace $p$ will communicate over $w$ instead of $x$. (It is straightforward to generalise this construction to arbitrarily many names, and to offer it through syntactic sugar, e.g., $\let\tilde{x}=\tilde{w}\in P$.) This is often done in practice, e.g., in the setting of microservices [?]; for example, in the Jolie programming language, the constructs of aggregation and embedding are used to implement this pattern [?], but without any type safety guarantees on the usage of sessions as in CHOP.

In [?] and [?], the notion of duality found in linear logic is replaced with coherence, which allows many processes to participate in a same session. We leave an extension of CHOP to such multiparty sessions to future work.

The calculus of Linear Compositional Choreographies (LCC) [?] gives a propositions-as-types correspondence for Choreographic Programming [?] based on linear logic. CHOP may provide the basis for extending LCC with process mobility, potentially yielding the first higher-order choreography calculus.

# 4 Conclusions

We presented CHOP, an attempt at extending CP to higher-order process communication. This paper is meant as a first attempt at formulating its theory. The reductions supported by CHOP, derived by sound proof transformations, are promising in the sense that: they realise communication as expected; they preserve typing; and they point out how process substitutions may be implemented efficiently (applied only where they are needed), recalling explicit substitutions for the $\lambda$-calculus [?].

We have deliberately postponed presenting the metatheory for CHOP. The reason is that its main results require careful formulation, since differently from CP it makes sense for processes to get stuck (in CP, well-typed processes always progress). For example, the process $(\nu x^{\perp\gamma_1}y)(x(y).y().x[] | p)$ cannot reduce because of the free process variable $p$. We conjecture that a progress result can be formulated by appropriately instantiating free process variables whenever they are needed, similarly to how catalyser processes can be used in standard session types to provide all missing communication endpoints [?].

We end this work with an open question on expressivity. One of the reasons for which the standard $\pi$-calculus does not include process mobility is that it can be simulated through channel mobility. Now that we have an extension of CP to process mobility, can we prove the same result for CHOP? This would provide additional confidence on the fact that the propositions-as-types correspondence between linear logic propositions and session types is on the right track.

*Acknowledgements.* The author thanks Luís Cruz-Filipe and the anonymous reviewers for their useful comments. This work was supported by the CRC project, grant no. DFF-4005-00304 from the Danish Council for Independent Research, and by the Open Data Framework project at the University of Southern Denmark.