On Polymorphic Sessions and Functions

Syntax. Given an infinite set \(\varLambda \) of names x, y, z, u, v, the grammar of processes P, Q, R and session types A, B, C is defined by:\(x\langle y\rangle .P\) denotes the output of channel y on x with continuation process P; x(y).P denotes an input along x, bound to y in P; \(P\mid Q\) denotes parallel composition; \((\mathbf {\nu }y)P\) denotes the restriction of name y to the scope of P; \(\mathbf{0}\) denotes the inactive process; \([x\leftrightarrow y]\) denotes the linking of the two channels x and y (implemented as renaming); \(x\langle A \rangle .P\) and x(Y).P denote the sending and receiving of a type A along x bound to Y in P of the receiver process; \(x.\mathsf {inl};P\) and \(x.\mathsf {inr};P\) denote the emission of a selection between the \(\mathsf {l}\)eft or \(\mathsf {r}\)ight branch of a receiver \(x.\mathsf {case}(P,Q)\) process; \(!x(y).P\) denotes an input-guarded replication, that spawns replicas upon receiving an input along x. We often abbreviate \((\mathbf {\nu }y)x\langle y \rangle .P\) to \(\overline{x}\langle y \rangle .P\) and omit trailing \(\mathbf{0}\) processes. By convention, we range over linear channels with x, y, z and shared channels with u, v, w.

The syntax of session types is that of (intuitionistic) linear logic propositions which are assigned to channels according to their usages in processes: \(\mathbf {1}\) denotes the type of a channel along which no further behaviour occurs; denotes a session that waits to receive a channel of type A and will then proceed as a session of type B; dually, \(A~\otimes ~B\) denotes a session that sends a channel of type A and continues as B; \( A~ \& ~B\) denotes a session that offers a choice between proceeding as behaviours A or B; \(A \oplus B\) denotes a session that internally chooses to continue as either A or B, signalling appropriately to the communicating partner; \(!A\) denotes a session offering an unbounded (but finite) number of behaviours of type A; \(\forall X.A\) denotes a polymorphic session that receives a type B and behaves uniformly as \(A\{B/X\}\); dually, \(\exists X.A\) denotes an existentially typed session, which emits a type B and behaves as \(A\{B/X\}\).

Operational Semantics. The operational semantics of our calculus is presented as a standard labelled transition system (Fig. 1) in the style of the early system for the \(\pi \)-calculus [46].

In the remainder of this work we write \(\equiv \) for a standard \(\pi \)-calculus structural congruence extended with the clause \([x\leftrightarrow y] \equiv [y\leftrightarrow x]\). In order to streamline the presentation of observational equivalence [7, 36], we write \(\equiv _!\) for structural congruence extended with the so-called sharpened replication axioms [46], which capture basic equivalences of replicated processes (and are present in the proof dynamics of the exponential of linear logic). A transition \(P \xrightarrow {~\alpha ~} Q\) denotes that P may evolve to Q by performing the action represented by label \(\alpha \). An action \(\alpha \) (\(\overline{\alpha }\)) requires a matching \(\overline{\alpha }\) (\(\alpha \)) in the environment to enable progress. Labels include: the silent internal action \(\tau \), output and bound output actions (\(\overline{x\langle y\rangle }\) and \(\overline{(\nu z)x\langle z\rangle }\)); input action x(y); the binary choice actions (\(x.\mathsf {inl}\), \(\overline{x.\mathsf {inl}}\), \(x.\mathsf {inr}\), and \(\overline{x.\mathsf {inr}}\)); and output and input actions of types (\(\overline{x\langle A\rangle }\) and x(A)).

The labelled transition relation is defined by the rules in Fig. 1, subject to the side conditions: in rule \((\mathsf {res})\), we require \(y\not \in { fn}(\alpha )\); in rule \((\mathsf {par})\), we require \({ bn}(\alpha ) \cap { fn}(R) = \emptyset \); in rule \((\mathsf {close})\), we require \(y\not \in { fn}(Q)\). We omit the symmetric versions of \((\mathsf {par})\), \((\mathsf {com})\), \((\mathsf {lout})\), \((\mathsf {lin})\), \((\mathsf {close})\) and closure under \(\alpha \)-conversion. We write \(\rho _1 \rho _2\) for the composition of relations \(\rho _1, \rho _2\). We write \(\xrightarrow {}\) to stand for \(\xrightarrow {\tau }\equiv \). Weak transitions are defined as usual: we write \({\mathop {\Longrightarrow }\limits ^{}}\) for the reflexive, transitive closure of \(\xrightarrow {\tau }\) and \(\xrightarrow {}^+\) for the transitive closure of \(\xrightarrow {\tau }\). Given \(\alpha \ne \tau \), notation \({\mathop {\Longrightarrow }\limits ^{\alpha }}\) stands for \({\mathop {\Longrightarrow }\limits ^{~}}\xrightarrow {\alpha }{\mathop {\Longrightarrow }\limits ^{~}}\) and \({\mathop {\Longrightarrow }\limits ^{\tau }}\) stands for \({\mathop {\Longrightarrow }\limits ^{}}\).

Typing System. The typing rules of Poly\(\pi \) are given in Fig. 2, following [7]. The rules define the judgment \(\varOmega ; \varGamma ; \varDelta \vdash P~{:}{:}~z{:}A\), denoting that process P offers a session of type A along channel z, using the linear sessions in \(\varDelta \), (potentially) using the unrestricted or shared sessions in \(\varGamma \), with polymorphic type variables maintained in \(\varOmega \). We use a well-formedness judgment \(\varOmega \vdash A\,\mathsf {type}\) which states that A is well-formed wrt the type variable environment \(\varOmega \) (i.e. \( fv (A) \subseteq \varOmega \)). We often write T for the right-hand side typing z : A, \(\cdot \) for the empty context and \(\varDelta ,\varDelta '\) for the union of contexts \(\varDelta \) and \(\varDelta '\), only defined when \(\varDelta \) and \(\varDelta '\) are disjoint. We write \(\cdot \vdash P~{:}{:}~T\) for \(\cdot ; \cdot ; \cdot \vdash P~{:}{:}~T\).

As in [8, 9, 36, 54], the typing discipline enforces that channel outputs always have as object a fresh name, in the style of the internal mobility \(\pi \)-calculus [44]. We clarify a few of the key rules: Rule \({{\forall }\mathsf {R}}\) defines the meaning of (impredicative) universal quantification over session types, stating that a session of type \(\forall X.A\) inputs a type and then behaves uniformly as A; dually, to use such a session (rule \({{\forall }\mathsf {L}}\)), a process must output a type B which then warrants the use of the session as type \(A\{B/X\}\). Rule captures session input, where a session of type expects to receive a session of type A which will then be used to produce a session of type B. Dually, session output (rule \({{\otimes }\mathsf {R}}\)) is achieved by producing a fresh session of type A (that uses a disjoint set of sessions to those of the continuation) and outputting the fresh session along z, which is then a session of type B. Linear composition is captured by rule \(\mathsf {cut}\) which enables a process that offers a session x : A (using linear sessions in \(\varDelta _1\)) to be composed with a process that uses that session (amongst others in \(\varDelta _2\)) to offer z : C. As shown in [7], typing entails Subject Reduction, Global Progress, and Termination.

Observational Equivalences. We briefly summarise the typed congruence and logical equivalence with polymorphism, giving rise to a suitable notion of relational parametricity in the sense of Reynolds [41], defined as a contextual logical relation on typed processes [7]. The logical relation is reminiscent of a typed bisimulation. However, extra care is needed to ensure well-foundedness due to impredicative type instantiation. As a consequence, the logical relation allows us to reason about process equivalences where type variables are not instantiated with the same, but rather related types.

Typed Barbed Congruence ( ). We use the typed contextual congruence from [7], which preserves observable actions, called barbs. Formally, barbed congruence, noted , is the largest equivalence on well-typed processes that is \(\tau \)-closed, barb preserving, and contextually closed under typed contexts; see [7, 52] for the full definition.

Logical Equivalence ( ). The definition of logical equivalence is no more than a typed contextual bisimulation with the following intuitive reading: given two open processes P and Q (i.e. processes with non-empty left-hand side typings), we define their equivalence by inductively closing out the context, composing with equivalent processes offering appropriately typed sessions. When processes are closed, we have a single distinguished session channel along which we can perform observations, and proceed inductively on the structure of the offered session type. We can then show that such an equivalence satisfies the necessary fundamental properties (Theorem 2.3).

The logical relation is defined using the candidates technique of Girard [16]. In this setting, an equivalence candidate is a relation on typed processes satisfying basic closure conditions: an equivalence candidate must be compatible with barbed congruence and closed under forward and converse reduction.

To define the logical relation we rely on some auxiliary notation, pertaining to the treatment of type variables arising due to impredicative polymorphism. We write \(\omega : \varOmega \) to denote a mapping \(\omega \) that assigns a closed type to the type variables in \(\varOmega \). We write \(\omega (X)\) for the type mapped by \(\omega \) to variable X. Given two mappings \(\omega : \varOmega \) and \(\omega ' : \varOmega \), we define an equivalence candidate assignment \(\eta \) between \(\omega \) and \(\omega '\) as a mapping of equivalence candidate \(\eta (X)~{:}{:}~{-}{:}\omega (X)\,\!\Leftrightarrow \!\,\omega '(X)\) to the type variables in \(\varOmega \), where the particular choice of a distinguished right-hand side channel is delayed (i.e. to be instantiated later on). We write \(\eta (X)(z)\) for the instantiation of the (delayed) candidate with the name z. We write \(\eta : \omega ~\!\Leftrightarrow \!~\omega '\) to denote that \(\eta \) is a candidate assignment between \(\omega \) and \(\omega '\); and \(\hat{\omega }(P)\) to denote the application of mapping \(\omega \) to P.

We define a sequent-indexed family of process relations, that is, a set of pairs of processes (P, Q), written \(\varGamma ; \varDelta \vdash P \approx _{\mathtt {L}}Q~{:}{:}~ T [\eta : \omega \,\!\Leftrightarrow \!\,\omega ']\), satisfying some conditions, typed under \(\varOmega ; \varGamma ; \varDelta \vdash T\), with \(\omega : \varOmega \), \(\omega ' : \varOmega \) and \(\eta : \omega \,\!\Leftrightarrow \!\,\omega '\). Logical equivalence is defined inductively on the size of the typing contexts and then on the structure of the right-hand side type. We show only select cases (see [52] for the full definition).

For the sake of readability we often omit the \(\eta : \omega ~\!\Leftrightarrow \!~ \omega '\) portion of , which is henceforth implicitly universally quantified. Thus, we write (or ) iff the two given processes are logically equivalent for all consistent instantiations of its type variables.

It is instructive to inspect the clause for type input (\(\forall X.A\)): the two processes must be able to match inputs of any pair of related types (i.e. types related by a candidate), such that the continuations are related at the open type A with the appropriate type variable instantiations, following Girard [16]. The power of this style of logical relation arises from a combination of the extensional flavour of the equivalence and the fact that polymorphic equivalences do not require the same type to be instantiated in both processes, but rather that the types are related (via a suitable equivalence candidate relation).

We define a translation from Linear-F to Poly\(\pi \) generalising the one from [49], accounting for polymorphism and multiplicative pairs. We translate typing derivations of \(\lambda \)-terms to those of \(\pi \)-calculus terms (we omit the full typing derivation for the sake of readability).

Proof theoretically, the \(\lambda \)-calculus corresponds to a proof term assignment for natural deduction presentations of logic, whereas the session \(\pi \)-calculus from § 2 corresponds to a proof term assignment for sequent calculus. Thus, we obtain a translation from \(\lambda \)-calculus to the session \(\pi \)-calculus by considering the proof theoretic content of the constructive proof of soundness of the sequent calculus wrt natural deduction. Following Gentzen [14], the translation from natural deduction to sequent calculus maps introduction rules to the corresponding right rules and elimination rules to a combination of the corresponding left rule, cut and/or identity.

Since typing in the session calculus identifies a distinguished channel along which a process offers a session, the translation of \(\lambda \)-terms is parameterised by a “result” channel along which the behaviour of the \(\lambda \)-term is implemented. Given a \(\lambda \)-term M, the process \(\llbracket M \rrbracket _z\) encodes the behaviour of M along the session channel z. We enforce that the type \(\mathbf {2}\) of booleans and its two constructors are consistently translated to their polymorphic Church encodings before applying the translation to Poly\(\pi \). Thus, type \(\mathbf {2}\) is first translated to , the value \(\mathsf {T}\) to and the value \(\mathsf {F}\) to . Such representations of the booleans are adequate up to parametricity [6] and suitable for our purposes of relating the session calculus (which has no primitive notion of value or result type) with the \(\lambda \)-calculus precisely due to the tight correspondence between the two calculi.

To translate a (linear) \(\lambda \)-abstraction \(\lambda x{:}A.M\), which corresponds to the proof term for the introduction rule for , we map it to the corresponding rule, thus obtaining a process \(z(x).\llbracket M\rrbracket _z\) that inputs along the result channel z a channel x which will be used in \(\llbracket M\rrbracket _z\) to access the function argument. To encode the application \(M\,N\), we compose (i.e. \(\mathsf {cut}\)) \(\llbracket M\rrbracket _x\), where x is a fresh name, with a process that provides the (encoded) function argument by outputting along x a channel y which offers the behaviour of \(\llbracket N\rrbracket _y\). After the output is performed, the type of x is now that of the function’s codomain and thus we conclude by forwarding (i.e. the \(\mathsf {id}\) rule) between x and the result channel z.

The encoding for polymorphism follows a similar pattern: To encode the abstraction \(\varLambda X.M\), we receive along the result channel a type that is bound to X and proceed inductively. To encode type application M[A] we encode the abstraction M in parallel with a process that sends A to it, and forwards accordingly. Finally, the encoding of the existential package maps to an output of the type A followed by the behaviour \(\llbracket M \rrbracket _z\), with the encoding of the elimination form composing the translation of the term of existential type M with a process performing the appropriate type input and proceeding as \(\llbracket N \rrbracket _z\).

Just as the proof theoretic content of the soundness of sequent calculus wrt natural deduction induces a translation from \(\lambda \)-terms to session-typed processes, the completeness of the sequent calculus wrt natural deduction induces a translation from the session calculus to the \(\lambda \)-calculus. This mapping identifies sequent calculus right rules with the introduction rules of natural deduction and left rules with elimination rules combined with (type-preserving) substitution. Crucially, the mapping is defined on typing derivations, enabling us to consistently identify when a process uses a session (i.e. left rules) or, dually, when a process offers a session (i.e. right rules).

For instance, the encoding of a process , typed by rule , results in the corresponding introduction rule in the \(\lambda \)-calculus and thus is . To encode the process \((\mathbf {\nu }y)x\langle y \rangle .(P \mid Q)\), typed by rule , we make use of substitution: Given that the sub-process Q is typed as \(\varOmega ; \varGamma ; \varDelta ' , x{:}B \vdash Q~{:}{:}~z{:}C\), the encoding of the full process is given by . The term consists of the application of x (of function type) to the argument , thus ensuring that the term resulting from the substitution is of the appropriate type. We note that, for instance, the encoding of rule \({{\otimes }\mathsf {L}}\) does not need to appeal to substitution – the \(\lambda \)-calculus \(\mathsf {let}\) style rules can be mapped directly. Similarly, rule \({{\forall }\mathsf {R}}\) is mapped to type abstraction, whereas rule \({{\forall }\mathsf {L}}\) which types a process of the form \(x\langle B \rangle .P\) maps to a substitution of the type application x[B] for x in . The encoding of existential polymorphism is simpler due to the \(\mathsf {let}\)-style elimination. We also highlight the encoding of the \(\mathsf {cut}\) rule which embodies parallel composition of two processes sharing a linear name, which clarifies the use/offer duality of the intuitionistic calculus – the process that offers P is encoded and substituted into the encoded user Q.

In general, the translation of Definition 3.5 can introduce some distance between the immediate operational behaviour of a process and its corresponding \(\lambda \)-term, insofar as the translations of cuts (and left rules to non \(\mathsf {let}\)-form elimination rules) make use of substitutions that can take place deep within the resulting term. Consider the process at the root of the following typing judgment , derivable through a \(\mathsf {cut}\) on session x between instances of and , where the continuation process \(w(z).\mathbf{0}\) offers a session (and so must use rule \({{\mathbf {1}}\mathsf {L}}\) on x). We have that: \((\mathbf {\nu }x)(x(y).P_1 \mid (\mathbf {\nu }y)x\langle y \rangle .(P_2 \mid w(z).\mathbf{0})) \xrightarrow {} (\mathbf {\nu }x,y)(P_1 \mid P_2 \mid w(z).\mathbf{0})\). However, the translation of the process above results in the term , where the redex that corresponds to the process reduction is present but hidden under the binder for z (corresponding to the input along w). Thus, to establish operational completeness we consider full \(\beta \)-reduction, denoted by \(\xrightarrow {}_\beta \), i.e. enabling \(\beta \)-reductions under binders.

In order to study the soundness direction it is instructive to consider typed process and its translation:The process above cannot reduce due to the output prefix on x, which cannot synchronise with a corresponding input action since there is no provider for x (i.e. the channel is in the left-hand side context). However, its encoding can exhibit the \(\beta \)-redex corresponding to the synchronisation along z, hidden by the prefix on x. The corresponding reductions hidden under prefixes in the encoding can be soundly exposed in the session calculus by appealing to the commuting conversions of linear logic (e.g. in the process above, the instance of rule corresponding to the output on x can be commuted with the \(\mathsf {cut}\) on z).

As shown in [36], commuting conversions are sound wrt observational equivalence, and thus we formulate operational soundness through a notion of extended process reduction, which extends process reduction with the reductions that are induced by commuting conversions. Such a relation was also used for similar purposes in [5] and in [26], in a classical linear logic setting. For conciseness, we define extended reduction as a relation on typed processes modulo \(\equiv \).

Having established the operational preciseness of the encodings to-and-from Poly\(\pi \) and Linear-F, we establish our main results for the encodings. Specifically, we show that the encodings are mutually inverse up-to behavioural equivalence (with fullness as its corollary), which then enables us to establish full abstraction for both encodings.

We now state our full abstraction results. Given two Linear-F terms of the same type, equivalence in the image of the \(\llbracket {-}\rrbracket _z\) translation can be used as a proof technique for contextual equivalence in Linear-F. This is called the soundness direction of full abstraction in the literature [18] and proved by showing the relation generated by forms ; we then establish the completeness direction by contradiction, using fullness.

We can straightforwardly combine the above full abstraction with Theorem 3.11 to obtain full abstraction of the translation.

The study of polymorphism in the \(\lambda \)-calculus [1, 6, 19, 40] has shown that parametric polymorphism is expressive enough to encode both inductive and coinductive types in a precise way, through a faithful representation of initial and final (co)algebras [28], without extending the language of terms nor the semantics of the calculus, giving a logical justification to the Church encodings of inductive datatypes such as lists and natural numbers. The polymorphic session calculus can express fairly intricate communication behaviours, including generic protocols through both existential and universal polymorphism (i.e. protocols that are parametric in their sub-protocols). Using our fully abstract encodings between the two calculi, we show that session polymorphism is expressive enough to encode inductive and coinductive sessions, “importing” the results for the \(\lambda \)-calculus, which may then be instantiated to provide a session-typed formulation of the encodings of data structures in the \(\pi \)-calculus of [30].

Inductive and Coinductive Types in System F. Exploring an algebraic interpretation of polymorphism where types are interpreted as functors, it can be shown that given a type F with a free variable X that occurs only positively (i.e. occurrences of X are on the left-hand side of an even number of function arrows), the polymorphic type \(\forall X.((F(X) \rightarrow X) \rightarrow X)\) forms an initial F-algebra [1, 42] (we write F(X) to denote that X occurs in F). This enables the representation of inductively defined structures using an algebraic or categorical justification. For instance, the natural numbers can be seen as the initial F-algebra of \(F(X) = \mathbf {1}+ X\) (where \(\mathbf {1}\) is the unit type and \(+\) is the coproduct), and are thus already present in System F, in a precise sense, as the type \(\forall X.((\mathbf {1}+ X) \rightarrow X) \rightarrow X\) (noting that both \(\mathbf {1}\) and \(+\) can also be encoded in System F). A similar story can be told for coinductively defined structures, which correspond to final F-coalgebras and are representable with the polymorphic type \(\exists X. (X \rightarrow F(X)) \times X\), where \(\times \) is a product type. In the remainder of this section we assume the positivity requirement on F mentioned above.

While the complete formal development of the representation of inductive and coinductive types in System F would lead us to far astray, we summarise here the key concepts as they apply to the \(\lambda \)-calculus (the interested reader can refer to [19] for the full categorical details).

To show that the polymorphic type \(T_i \triangleq \forall X.((F(X) \rightarrow X) \rightarrow X)\) is an initial F-algebra, one exhibits a pair of \(\lambda \)-terms, often dubbed \(\mathsf {fold}\) and \(\mathsf {in}\), such that the diagram in Fig. 4(a) commutes (for any A, where F(f), where f is a \(\lambda \)-term, denotes the functorial action of F applied to f), and, crucially, that \(\mathsf {fold}\) is unique. When these conditions hold, we are justified in saying that \(T_i\) is a least fixed point of F. Through a fairly simple calculation, it is easy to see that:satisfy the necessary equalities. To show uniqueness one appeals to parametricity, which allows us to prove that any function of the appropriate type is equivalent to \(\mathsf {fold}\). This property is often dubbed initiality or universality.

The construction of final F-coalgebras and their justification as greatest fixed points is dual. Assuming products in the calculus and taking \(T_f \triangleq \exists X. (X \rightarrow F(X)) \times X\), we produce the \(\lambda \)-termssuch that the diagram in Fig. 4(b) commutes and \(\mathsf {unfold}\) is unique (again, up to parametricity). While the argument above applies to System F, a similar development can be made in Linear-F [6] by considering and . Reusing the same names for the sake of conciseness, the associated linear \(\lambda \)-terms are:Inductive and Coinductive Sessions for Free. As a consequence of full abstraction we may appeal to the \(\llbracket {-}\rrbracket _z\) encoding to derive representations of \(\mathsf {fold}\) and \(\mathsf {unfold}\) that satisfy the necessary algebraic properties. The derived processes are (recall that we write \(\overline{x}\langle y \rangle .P\) for \((\mathbf {\nu }y)x\langle y \rangle .P\)):We can then show universality of the two constructions. We write \(P_{x,y}\) to single out that x and y are free in P and \(P_{z,w}\) to denote the result of employing capture-avoiding substitution on P, substituting x and y by z and w. Let:where \(\mathsf {foldP}(A)_{y_1,y_2}\) corresponds to the application of \(\mathsf {fold}\) to an F-algebra A with the associated morphism available on the shared channel u, consuming an ambient session \(y_1{:}T_i\) and offering \(y_2{:}A\). Similarly, \(\mathsf {unfoldP}(A)_{y_1,y_2}\) corresponds to the application of \(\mathsf {unfold}\) to an F-coalgebra A with the associated morphism available on the shared channel u, consuming an ambient session \(y_1{:}A\) and offering \(y_2{:}T_f\).

We now consider a session calculus extended with a data layer obtained from a \({\lambda }\)-calculus (whose terms are ranged over by M, N and types by \({\tau ,\sigma }\)). We dub this calculus Sess\(\pi \lambda \).Without loss of generality, we consider the data layer to be simply-typed, with a call-by-name semantics, satisfying the usual type safety properties. The typing judgment for this calculus is \(\varPsi \vdash M : \tau \). We omit session polymorphism for the sake of conciseness, restricting processes to communication of data and (session) channels. The typing judgment for processes is thus modified to \(\varPsi ; \varGamma ; \varDelta \vdash P~{:}{:}~z{:}A\), where \(\varPsi \) is an intuitionistic context that accounts for variables in the data layer. The rules for the relevant process constructs are (all other rules simply propagate the \(\varPsi \) context from conclusion to premises):With the reduction rule given by:¹ \( x\langle M \rangle . P \mid x(y).Q \xrightarrow {} P \mid Q\{M/y\} \). With a simple extension to our encodings we may eliminate the data layer by encoding the data objects as processes, showing that from an expressiveness point of view, data communication is orthogonal to the framework. We note that the data language we are considering is not linear, and the usage discipline of data in processes is itself also not linear.

To First-Order Processes. We now introduce our encoding for Sess\(\pi \lambda \), defined inductively on session types, processes, types and \(\lambda \)-terms (we omit the purely inductive cases on session types and processes for conciseness). As before, the encoding on processes is defined on typing derivations, where we indicate the typing rule at the root of the typing derivation. The encoding addresses the non-linear usage of data elements in processes by encoding the types \({\tau \wedge A}\) and \(\tau \supset A\) as \({!\llbracket \tau \rrbracket \otimes \llbracket A\rrbracket }\) and , respectively. Thus, sending and receiving of data is codified as the sending and receiving of channels of type \(!\), which therefore can be used non-linearly. Moreover, since data terms are themselves non-linear, the \({\tau \rightarrow \sigma }\) type is encoded as , following Girard’s embedding of intuitionistic logic in linear logic [15].

At the level of processes, offering a session of type \(\tau \wedge A\) (i.e. a process of the form \(z\langle M \rangle .P\)) is encoded according to the translation of the type: we first send a fresh name x which will be used to access the encoding of the term M. Since M can be used an arbitrary number of times by the receiver, we guard the encoding of M with a replicated input, proceeding with the encoding of P accordingly. Using a session of type \(\tau \supset A\) follows the same principle. The input cases (and the rest of the process constructs) are completely homomorphic.

The encoding of \(\lambda \)-terms follows Girard’s decomposition of the intuitionistic function space [49]. The \(\lambda \)-abstraction is translated as input. Since variables in a \(\lambda \)-abstraction may be used non-linearly, the case for variables and application is slightly more intricate: to encode the application \(M\, N\) we compose M in parallel with a process that will send the “reference” to the function argument N which will be encoded using replication, in order to handle the potential for 0 or more usages of variables in a function body. Respectively, a variable is encoded by performing an output to trigger the replication and forwarding accordingly. Without loss of generality, we assume variable names and their corresponding replicated counterparts match, which can be achieved through \(\alpha \)-conversion before applying the translation. We exemplify our encoding as follows:Properties of the Encoding. We discuss the correctness of our encoding. We can straightforwardly establish that the encoding preserves typing.

To show that our encoding is operationally sound and complete, we capture the interaction between substitution on \(\lambda \)-terms and the encoding into processes through logical equivalence. Consider the following reduction of a process:Given that substitution in the target session \(\pi \)-calculus amounts to renaming, whereas in the \(\lambda \)-calculus we replace a variable for a term, the relationship between the encoding of a substitution \(M\{N/x\}\) and the encodings of M and N corresponds to the composition of the encoding of M with that of N, but where the encoding of N is guarded by a replication, codifying a form of explicit non-linear substitution.

Revisiting the process to the left of the arrow in Eq. 1 we have:whereas the process to the right of the arrow is encoded as:While the reduction of the encoded process and the encoding of the reduct differ syntactically, they are observationally equivalent – the latter inlines the replicated process behaviour that is accessible in the former on x. Having characterised substitution, we establish operational correspondence for the encoding.

The process equivalence in Theorem 4.6 above need not be extended to account for data (although it would be relatively simple to do so), since the processes in the image of the encoding are fully erased of any data elements.

Back to \(\lambda \)-Terms. We extend our encoding of processes to \(\lambda \)-terms to Sess\(\pi \lambda \). Our extended translation maps processes to linear \(\lambda \)-terms, with the session type \(\tau \wedge A\) interpreted as a pair type where the first component is replicated. Dually, \(\tau \supset A\) is interpreted as a function type where the domain type is replicated. The remaining session constructs are translated as in § 3.2. The treatment of non-linear components of processes is identical to our previous encoding: non-linear functions \(\tau \rightarrow \sigma \) are translated to linear functions of type ; a process offering a session of type \(\tau \wedge A\) (i.e. a process of the form \(z\langle M \rangle .P\), typed by rule \({{\wedge }\mathsf {R}}\)) is translated to a pair where the first component is the encoding of M prefixed with \(!\) so that it may be used non-linearly, and the second is the encoding of P. Non-linear variables are handled at the respective binding sites: a process using a session of type \(\tau \wedge A\) is encoded using the elimination form for the pair and the elimination form for the exponential; similarly, a process offering a session of type \(\tau \supset A\) is encoded as a \(\lambda \)-abstraction where the bound variable is of type . Thus, we use the elimination form for the exponential, ensuring that the typing is correct. We illustrate our encoding:Properties of the Encoding. Unsurprisingly due to the logical correspondence between natural deduction and sequent calculus presentations of logic, our encoding satisfies both type soundness and operational correspondence (c.f. Theorems 3.6, 3.8 and 3.10). The full development can be found in [52].

Relating the Two Encodings. We prove the two encodings are mutually inverse and preserve the full abstraction properties (we write \(=_\beta \) and \(=_{\beta \eta }\) for \(\beta \)- and \(\beta \eta \)-equivalence, respectively).

The equivalences above are formulated between the composition of the encodings applied to P (resp. M) and the process (resp. \(\lambda \)-term) after applying the translation embedding the non-linear components into their linear counterparts. This formulation matches more closely that of § 3.3, which applies to linear calculi for which the target languages of this section are a strict subset (and avoids the formalisation of process equivalence with terms). We also note that in this setting, observational equivalence and \(\beta \eta \)-equivalence coincide [3, 31]. Moreover, the extensional flavour of includes \(\eta \)-like principles at the process level.

We establish full abstraction for the encoding of \(\lambda \)-terms into processes (Theorem 4.8) in two steps: The completeness direction (i.e. from left-to-right) follows from operational completeness and strong normalisation of the \(\lambda \)-calculus. The soundness direction uses operational soundness. The proof of Theorem 4.8 uses the same strategy of Theorem 3.14, appealing to the inverse theorems.

We extend the value-passing framework of the previous section, accounting for process-passing (i.e. the higher-order) in a session-typed setting. As shown in [50], we achieve this by adding to the data layer a contextual monad that encapsulates (open) session-typed processes as data values, with a corresponding elimination form in the process layer. We dub this calculus Sess\(\pi \lambda ^+\).The type \(\{ \overline{x_j{:}A_j} \vdash z{:}A\}\) is the type of a term which encapsulates an open process that uses the linear channels \(\overline{x_j{:}A_j}\) and offers A along channel z. This formulation has the added benefit of formalising the integration of session-typed processes in a functional language and forms the basis for the concurrent programming language SILL [37, 50]. The typing rules for the new constructs are (for simplicity we assume no shared channels in process monads):Rule \(\{\}I\) embeds processes in the term language by essentially quoting an open process that is well-typed according to the type specification in the monadic type. Dually, rule \(\{\}E\) allows for processes to use monadic values through composition that consumes some of the ambient channels in order to provide the monadic term with the necessary context (according to its type). These constructs are discussed in substantial detail in [50]. The reduction semantics of the process construct is given by (we tacitly assume that the names \(\overline{y}\) and c do not occur in P and omit the congruence case):The semantics allows for the underlying monadic term M to evaluate to a (quoted) process P. The process P is then executed in parallel with the continuation Q, sharing the linear channel c for subsequent interactions. We illustrate the higher-order extension with following typed process (we write \(\{x\leftarrow P\}\) when P does not depend on any linear channels and assume \(\vdash Q ~{:}{:}~d{:}\mathsf {Nat}\wedge \mathbf {1}\)):Process P above gives an abstract view of a communication idiom where a process (the left-hand side of the parallel composition) sends another process Q which potentially encapsulates some complex computation. The receiver then spawns the execution of the received process and inputs from it a result value that is sent back to the original sender. An execution of P is given by:Given the seminal work of Sangiorgi [46], such a representation naturally begs the question of whether or not we can develop a typed encoding of higher-order processes into the first-order setting. Indeed, we can achieve such an encoding with a fairly simple extension of the encoding of § 4.2 to Sess\(\pi \lambda ^+\) by observing that monadic values are processes that need to be potentially provided with extra sessions in order to be executed correctly. For instance, a term of type \(\{x{:}A\vdash y{:}B\}\) denotes a process that given a session x of type A will then offer y : B. Exploiting this observation we encode this type as the session , ensuring subsequent usages of such a term are consistent with this interpretation.To encode the monadic type \(\{ \overline{x_j{:}A_j} \vdash z{:}A\}\), denoting the type of process P that is typed by \(\overline{x_j{:}A_j} \vdash P~{:}{:}~z{:}A\), we require that the session in the image of the translation specifies a sequence of channel inputs with behaviours \(\overline{A_j}\) that make up the linear context. After the contextual aspects of the type are encoded, the session will then offer the (encoded) behaviour of A. Thus, the encoding of the monadic type is , which we write as . The encoding of monadic expressions adheres to this behaviour, first performing the necessary sequence of inputs and then proceeding inductively. Finally, the encoding of the elimination form for monadic expressions behaves dually, composing the encoding of the monadic expression with a sequence of outputs that instantiate the consumed names accordingly (via forwarding). The encoding of process P from Eq. 2 is thus:Properties of the Encoding. As in our previous development, we can show that our encoding for Sess\(\pi \lambda ^+\) is type sound and satisfies operational correspondence. The full development is omitted but can be found in [52].

We encode Sess\(\pi \lambda ^+\) into \(\lambda \)-terms, extending § 4.2 with:The encoding translates the monadic type \(\{\overline{x_i{:}A_i} \vdash z{:} A\}\) as a linear function , which captures the fact that the underlying value must be provided with terms satisfying the requirements of the linear context. At the level of terms, the encoding for the monadic term constructor follows its type specification, generating a nesting of \(\lambda \)-abstractions that closes the term and proceeding inductively. For the process encoding, we translate the monadic application construct analogously to the translation of a linear \(\mathsf {cut}\), but applying the appropriate variables to the translated monadic term (which is of function type). We remark the similarity between our encoding and that of the previous section, where monadic terms are translated to a sequence of inputs (here a nesting of \(\lambda \)-abstractions). Our encoding satisfies type soundness and operational correspondence, as usual. Further showcasing the applications of our development, we obtain a novel strong normalisation result for this higher-order session-calculus “for free”, through encoding to the \(\lambda \)-calculus.