A Continuation-Based Solution of the Linearity Challenge

Abstract The formalisation of session calculi is made difficult by the management of session channels, which are linear resources that cannot be discarded or duplicated and whose type changes over time, as input/output operations are performed on them. Context splitting, the channel management technique directly related to the way session type theories are usually written with pen and paper, is often considered a hindrance and a notable source of complexity, to the point where several alternative approaches have been recently proposed. In this paper we describe the Agda formalisation of a process calculus based on classical linear logic that supports the modeling of binary sessions through their encoding with explicit continuation channels. The formalisation turns out to be remarkably compact despite the adoption of context splitting. We argue that the logical nature of the calculus and the use of explicit continuations are contributing factors to the simplicity of its formalisation. 1 Introduction The Concurrent Calculi Formalisation Benchmark [6] is a collection of challenges concerning the mechanisation of core models of concurrent and distributed programming languages. These models often make use of distinctive features that set them apart from the models of sequential programming languages, such as the adoption of substructural (linear, affine) type systems, the dynamic scope of first-class channels in systems of communicating processes, and the need for coinductive definitions and proof methods for describing and reasoning on possibly infinite behaviours. The benchmark aims at identifying effective formalisation techniques that take these features into account so as to foster the adoption of machine-checked proofs in research work concerning concurrent and distributed programming languages. One of the challenges in the benchmark, henceforth called linearity challenge, concerns the formalisation of a minimal calculus of sessions. Sessions and session types [15, 18, 19, 21] are established abstractions for the static analysis of distributed programs based on peer-to-peer communications. Every session-typed system revolves around three key ideas: (1) session endpoints can only be used sequentially and cannot be discarded or duplicated without compromising some safety and liveness properties of a program; (2) the type of a session endpoint is updated after each use to reflect the state of the protocol it describes; (3) peer session endpoints are meant to be used in complementary ways so as to guarantee the absence of communication errors and, to some extent, progress of the interaction. The linearity challenge is based on the observation that the proper management of linear resources in a formalisation often requires a large number of auxiliary definitions and technical results that divert from the main problem under study [6]. One of the alleged culprits of such complexity is context splitting, namely the operation that partitions a typing context in such a way that the linear resources described therein end up in only one of the partitions. This observation has led to the exploration of various alternative techniques including leftover typing [43], the use of linearity predicates [36] and tagged contexts [42]. In this paper we approach the linearity challenge from a different angle: instead of proposing new techniques that make it easy to formalise the calculus in the challenge, we propose a (relatively) new calculus that is easy to formalise with the existing techniques. More specifically, we describe the Linear Calculus of Continuations (LCC) whose type system coincides with the proof system of classical linear logic and that features linear channels instead of sessions. While a session endpoint can be used multiple times (sequentially), linear channels must be used exactly once. LCC retains the expressiveness of other session calculi thanks to explicit continuations, which enable the encoding of (binary) sessions in terms of linear channels [11, 26]. Each message exchanged on a linear channel may include one or two fresh channels—the continuations – on which the rest of the communication takes place. Roughly speaking, LCC stands in between CP [40]—Wadler’s calculus of sessions based on classical linear logic—and the interpretation of linear logic proofs as \(\pi \)-calculus processes studied by Abramsky [1] and by Bellin and Scott [3]. While CP features native sessions, LCC and the interpretations by Abramsky, Bellin and Scott [1, 3] make use of explicit continuations. While both CP and LCC provide native process forms corresponding to the additive connectives of the logic, Abramsky et al. [1, 3] encode them using affine—“use-at-most-once”—channels. The logical foundations of LCC and the use of explicit continuations play an important role in taming the complexity of the formalisation. Working with a calculus based on linear logic prevents by construction the same (sequential) process to own both endpoints of a session, which is undesirable since it does not correspond to a useful pattern of interaction (every meaningful session requires its endpoints to be used by parallel processes) and is a potential source of deadlocks. From the standpoint of the formalisation, where the representation of channels is a primary design choice, it spares us the need to distinguish the two endpoints of a session, e.g. by means of polarities [13, 43] or by using different names connected by the same binder [15, 39]. Using a calculus with linear channels and explicit continuations spares us the need to update the type of channels in typing contexts. Once a channel has been used it is effectively consumed, and therefore its type is removed from the typing context. The continuation channel is fresh by definition, and therefore its type is added at the beginning of the typing context. As it turns out, removing and adding types is easier than updating them. The formalisation of LCC that we obtain is at the same time complete (in terms of features supported by the calculus) and streamlined (in terms of code size) compared to the known formalisations of session/linear calculi [7, 10, 16, 22, 35,36,37, 42, 43]. It is also one of only two formalisations that prove the deadlock freedom property for a session calculus [22], and it does so with substantially less code. The rest of the paper is organised as follows. Section 2 describes the syntax and the operational semantics of LCC and states the properties of well-typed processes that we formalise and prove, namely typing preservation, deadlock freedom and runtime safety. Section 3 illustrates the key aspects of the Agda formalisation with particular emphasis on the representation of channels and of typing contexts. We assume that the reader is somewhat familiar with Agda, but we recall the lesser known definitions from Agda’s standard library. Section 4 provides a more detailed description of the correspondence between CP and LCC. Section 5 discusses related work more in detail and includes a qualitative and quantitative comparison between the known formalisations of session/linear calculi. Section 6 summarises our contributions and discusses ongoing and future work. The formalisation has been checked with Agda 2.8.0 and the code is available in a public repository on GitHub [32]. 2 A Linear Calculus of Continuations In this section we give a cursory presentation of LCC starting from its types (Sect. 2.1), then moving on to the syntax of processes (Sect. 2.2), their reduction semantics (Sect. 2.3), the typing rules (Sect. 2.4) and the formulation of the properties ensured by the type system (Sect. 2.5). As we have anticipated in Sect. 1, LCC is closely related to CP [15, 40] except that LCC features linear channels instead of sessions. We refer the reader to the literature on CP [15, 29, 40] and other session calculi based on linear logic [4, 5] for a thorough introduction to these models. 2.1 Types The types of LCC, ranged over by \(A, B, \dots ,\) are the linear logic propositions generated by the grammar where \(X, Y, \dots \) range over an infinite set of type (or proposition) variables. The interpretation of linear logic propositions as behaviours is quite standard. Constants and connectives describe linear channels, which must be used for a single communication, whereas the modalities ! and ? describe shared channels. The multiplicative constants \(\bot \) and \(\textbf{1}\) describe channels used for receiving/sending an empty message (without continuations). The additive constants describe unusable channels. They can play the role of smallest/largest type in type systems that support a notion of subtyping [20], but we will mostly ignore them in this work. The additive connectives \( A { \& }B\) and \(A \oplus B\) describe channels used for receiving/sending either a continuation of type A or a continuation of type B. The sender selects one of the two possibilities, while the receiver offers both. The multiplicative connectives \(A \bindnasrepma B\) and \(A \otimes B\) describe channels used for receiving/sending two continuations, one of type A and the other of type B. The quantifiers \(\forall X.A\) and \(\exists X.A\) describe channels used for receiving/sending a type X along with a continuation of type A. They are useful to describe parametric protocol polymorphism. Finally, the “of course” modality !A and the “why not” modality ?A describe shared channels on which servers and clients accept and request connections of type A. The notions of free type variables, of duality and of type substitution are standard [40]. In particular, we write \(A^{\bot }\) for the dual of A and \(A\{B/X\}\) for the type obtained by replacing the free occurrences of X in A with B. 2.2 Processes The syntax of processes makes use of an infinite set of channels, ranged over by x, y and z, and is shown in Table 1. A link \(x\leftrightarrow y\) denotes the merging of the channels x and y, so that each message sent on one of the channels is forwarded to the other. As discussed in the literature [29] and illustrated in Example 2.2, this form is useful for sending an existing channel on another channel. The processes \(x().P\) and \(x[]\) respectively model the input and output of an empty message on the channel x. The latter process terminates after the message has been sent, while the former continues as P once the message has been received. The process \(x \triangleright \{\}\) can be used to denote a failure concerning the channel x. The process offers a choice on channel x and continues as either \(Q_1\) or \(Q_2\) depending on which branch is selected with z bound to the received continuation channel. The process performs a choice (represented by a label with \(i=1,2\)) and sends a fresh continuation channel z on the channel x. The processes x(y, z).R and x[y, z](P|Q) describe the input/output of two fresh continuations channels y and z on the channel x. The receiver can use y and z in whatever order. The sender forks into P and Q, each using y and z respectively. The processes \(x(X,z).P\) and \(x[A,z].P\) describe the input/output of a type on the channel x along with a fresh continuation z. Next we have process forms dealing with shared (non-linear) channels. The processes \({!}x(y).P\) and \({?}x[y].P\) respectively denote servers and clients acting on the shared channel x. Each request (from a client) spawns a copy of the server’s body using the continuation channel y. The process \({?}x[].P\) denotes an explicit weakening, that is a client that does not use x. The process \({?}x[y,z].P\) denotes an explicit contraction whereby a client uses x multiple times (once with name y and once with name z). Finally, cuts of the form (x : A)(P|Q) represent the parallel composition of the processes P and Q connected by a channel x, which has type A in P and type \(A^{\bot }\) in Q. Henceforth we write (x)(P|Q) omitting the type annotation A when it is irrelevant or clear from the context. The notions of free and bound channels are fairly standard, bearing in mind that output prefixes bind continuation channels in (some) continuation processes. For instance, binds z in P, while \(x[y,z]({P}|{Q})\) binds y in P but not in Q and binds z in Q but not in P. We write \(\textsf{fc}(P)\) for the set of channels occurring free in P and we identify processes up to renaming of bound channels. Example 2.1 We can represent the protocol of a boolean value being produced as the type \(\mathbb {B}{\mathop {=}\limits ^{\smash {\textsf {\small def}}}}\textbf{1}\oplus \textbf{1}\) and that of a boolean value being consumed as its dual \( \mathbb {B}^{\bot }= \bot { \& }\bot \). Following these types, the boolean constants can be modeled by the processes and the boolean negation function by the process As an example, the composition \((x:\mathbb {B})({\textit{True}(x)}|{\textit{Not}(x,y)})\) produces false on y. Note the use of explicit continuations in these processes and the fact that each channel is used exactly once. The same processes in CP would be written as where each channel is used multiple times to indicate the sequence of input/output actions pertaining to the same session. In general, the CP version of an LCC process can be obtained by reusing the same channel x in place of the continuation z in Table 1. We will make this intuition more precise in Sect. 4, where we informally discuss the equivalence of CP and LCC. \(\lrcorner \) 2.3 Operational Semantics The operational semantics of LCC is shown in Table 2 and is given by two relations: a structural pre-congruence relation \(\sqsupseteq \), which relates essentially indistinguishable processes, and a reduction relation \(\leadsto \), which models communications. Let us describe the two relations more in detail. Structural pre-congruence is the least pre-congruence defined by the [s-*] rules. [s-link] and [s-comm] assert that links and parallel compositions are commutative. The remaining rules, when read from left to right, push a cut on x underneath the topmost prefix on y of one of its sub-processes when \(x \ne y\). These rules are key to float input/output actions to the top-level of a process, so that they can interact with corresponding complementary actions in the surrounding context. All these rules have implicit side-conditions (not shown in Table 2) aimed at preserving the meaning of channels when binders are moved around: terms entering or exiting the scope of a binder for x must not have free occurrences of x. This holds also for the type variable X in the rule [s-forall]. We content ourselves with such informal description of these side conditions given that we are going to formalise LCC later on. Note also that there are two versions of [s-fork-l] and [s-fork-r] depending on which of the two continuations (either P or Q) contains a free occurrence of the restricted channel x. Another rule that deserves attention is [s-server]. In this case, a cut can be pushed underneath a server prefix \({!}y(u)\) only provided that the other process in the cut is also a server on the channel restricted by the cut. Reduction is defined by the [r-*] rules, most of them coinciding with principal cut reductions of linear logic. The rules [r-link], [r-close], [r-select], [r-fork] and [r-exists] erase the topmost cut and replace it with zero, one or two new cuts, depending on the number of continuation channels that are exchanged. Note that the rule [r-link] eliminates a link \(x\leftrightarrow y\) by substituting y for x in the scope of x and [r-close] models the communication of an empty message (without continuations). The rule [r-exists] models the instantiation of a polymorphic variable X as the communication of a type A. We write \(Q\{A/X\}\) for the process obtained by replacing every free occurrence of the type variable X with A. The rule [r-connect] models the connection between a client and a server, whereas the rules [r-weaken] and [r-contract] respectively model the disposal of an unused server and the duplication of a server. In these rules we use some slightly informal notation for denoting sequences of (pairwise distinct) channels and prefixes. In particular, \(\overline{z}\) stands for a sequence \(z_1, \dots , z_n\) of channels, \({?}\overline{z}[].Q\) stands for a sequence \({?}z_1[]\dots {?}z_n[].Q\) of weakening prefixes and \({?}\overline{z}[\overline{z}',\overline{z}''].R\) stands for a sequence \({?}z_1[z_1',z_1'']\dots {?}z_n[z_n',z_n''].R\) of contraction prefixes. The rule [r-cut] propagates reductions through cuts and the rule [r-cong] enables reduction up to structural pre-congruence. Example 2.2 In this example we illustrate the role of links for the communication of free channels by modeling an echo server that consumes boolean values and sends them back unchanged. The protocol of the server we want to model is described by the type \(!(\mathbb {B}^{\bot }\bindnasrepma (\mathbb {B}\otimes \textbf{1}))\) where the modality ! indicates that the server is able to accept an unbounded number of requests and the type \(\mathbb {B}^{\bot }\bindnasrepma (\mathbb {B}\otimes \textbf{1})\) describes the sequence of actions performed by the server at each connection with a client: the server first consumes a boolean value (say u, of type \(\mathbb {B}^{\bot }\)), then produces another boolean value (say v, of type \(\mathbb {B}\)) and finally sends an empty message. We can model the server and a possible client thus: Notice the use of continuations for chaining communications together. In the server, the link \(v\leftrightarrow u\) merges v and u so as to send the same channel u received from the client. In the client, the link \(v\leftrightarrow z\) “assigns” the message v received from the server to the free channel z, which represents the result of the interaction. If we write \(\leadsto ^*\) for the reflexive, transitive closure of \(\leadsto \) it is easy to verify that \((x)({\textit{Client}(x)}|{\textit{Server}(x)}) \leadsto ^* \textit{True}(z)\). \(\lrcorner \) 2.4 Type System We use typing contexts (i.e. sequents) to keep track of the type of channels in processes. Typing contexts are finite maps from channels to types written as \(x_1: A_1, \dots , x_n: A_n\) and ranged over by \(\Upgamma \) and \(\Updelta \). We write \(\Upgamma , \Updelta \) for the union of \(\Upgamma \) and \(\Updelta \) when they have disjoint domains. We write \(?\Upgamma \) for some context \(\Upgamma = x_1: ? A_1, \dots , x_n: ? A_n\) where all the types in its range are prefixed by the modality ?. We call these types unrestricted because they are used to denote shared channels that can be (explicitly) discarded and duplicated. Typing judgments have the form \(P\vdash \Upgamma \) meaning that the process P is well typed in the context \(\Upgamma \). Equivalently, the judgment indicates that the sequent \(\Upgamma \) is derivable and P is a proof term corresponding to the derivation for \(\Upgamma \). The typing rules are shown in Table 3. They are in one-to-one correspondence with—and have exactly the same structure as—the proof rules of classical linear logic. The reader may refer to the standard literature on propositions as sessions [15, 29, 40] for the interpretation of the rules. The only relevant difference with our typing rules is that the premises mentioning the continuation channel z actually refer to the same channel x on which the process in the conclusion is acting. The side condition \(X \not \in \textsf{fv}(\Upgamma )\) in the rule \([\exists ]\)checks that the type variable X does not occur free in the types of \({\Upgamma }\) and therefore can be generalised. Example 2.3 Looking at Example 2.3 we notice that the server does not make any assumption on the type of the values it receives and sends. Therefore, we can define a polymorphic version of the echo server that works for every message type and not just for the booleans. The polymorphic version of the echo server is defined below: The only difference with respect to the server in Example 2.3 is that now the process receives the type X of the messages to be processed and then continues as before. We establish that \(\textit{Server}(x)\) is well typed with the following derivation where the side condition of the rule \([\forall ]\)is trivially satisfied since the typing context does not contain bindings other than the one for y. \(\lrcorner \) 2.5 Properties of Well-Typed Processes The linearity challenge [6] aims at formalising two essential properties of well-typed processes: (1) typing is preserved by reductions; (2) the peer endpoints of the same session are always used in complementary ways. This latter property is called well formedness in the challenge. In this work we also consider deadlock freedom, which is more general than well formedness and holds for LCC since its type system is based on linear logic. We now formulate these properties using the notation developed so far. Concerning the preservation of typing, this corresponds to the usual subject reduction result, which is expressed thus: Theorem 2.1 (Subject reduction) If \(P \leadsto Q\) then \(P\vdash \Upgamma \) implies \({Q}\vdash \Upgamma \). In order to formulate deadlock freedom, we first need to introduce some terminology for referring to processes that are unable to make any progress. A simple example of deadlock is the process \((x)({x[]}|{x[]})\). This process is unable to reduce [because a process \(x[]\) is meant to interact with a process of the form \(x().P\)] and, more generally, it is unable to interact regardless of the context in which it is placed because the sub-processes it contains are blocked on the channel x that is restricted by the cut. In general, a deadlocked process is not simply a process that is unable to reduce; there are irreducible processes that are not a deadlock because they would be able to reduce if put into a suitable context. For example, \(x().P\) does not reduce, and yet it is not a deadlock because it would be able to make progress when composed in parallel with \(x[]\). Even a process like \((x)({y().P}|{z().Q})\) where \(x\ne y,z\) cannot be considered a deadlock, because the prefixes \(y()\) and \(z()\) could be exposed using [s-wait] and possibly [s-comm]. Let us make all this more precise. We say that P is a thread if it is anything but a cut. In other words, a thread is either a link or a process that starts with an input/output action of some sort. Note that a thread may contain cuts, but these cuts must be guarded underneath the topmost action prefix of the thread. We say that P is observable if \(P \sqsupseteq Q\) for some thread Q. An observable process is a process that exposes an action on a free channel and therefore can interact through that channel, if put into some appropriate context. We say that P is reducible if \(P \leadsto Q\) for some Q. A reducible process may perform a reduction step. We say that a process is alive if it is either observable or reducible and that it is a deadlock if it is not alive. Well-typed LCC processes are deadlock free: Theorem 2.2 (Deadlock freedom) If \({P}\vdash \Upgamma \) then P is alive. We now shift the attention to well formedness. In the linearity challenge [6] this property ensures that, whenever two processes composed in parallel begin with actions concerning the very same session, then such actions complement each other, in the sense that they describe opposite forms of interaction. To define well formedness in our setting, we introduce reduction contexts as partial processes with a single unguarded hole \([\,]\), thus: As usual, we write \(\mathcal {C}[P]\) for the process obtained by replacing the hole in \(\mathcal {C}\) with P, noting that such replacement may capture channels that are bound in \(\mathcal {C}\) and occur free in P. Now we observe that if \(Q_1\) and \(Q_2\) both act on the same channel x in complementary ways, then their parallel composition \((x)({Q_1}|{Q_2})\) is reducible according to one of the principal cut reductions described in Table 2. Therefore, an alternative (and more general) way of formulating well formedness is simply this: we say that P is well formed if \(P \sqsupseteq \mathcal {C}[Q]\) implies that Q is alive. In the particular case when \(Q = (x)({Q_1}|{Q_2})\) and both \(Q_1\) and \(Q_2\) start with an action on x, then Q is not observable (because actions on x cannot be pulled out of the cut that binds x) and therefore it must be reducible by Theorem 2.2. Well-typed processes are well formed: Theorem 2.3 (Type safety) If \({P}\vdash \Upgamma \) then P is well formed. Note that the properties expressed in Theorems 2.2 and 2.3 are invariant under reductions thanks to Theorem 2.1. 3 Agda Formalisation In this section we describe the formalisation of LCC in Agda. Each of the following sub-sections matches one of the modules of the formalisation. We present in detail only some key parts of the code including the representation of types and processes, the definition of the operational semantics and the statement of the main results. The complete source code is available in LCC ’s public repository [32]. 3.1 Type Representation The representation of types is standard. We start by defining an indexed data type to represent (LCC) types in the scope of n quantifiers, and we use elements of as de Bruijn indices for the quantified type variables. In this way, we make sure that pre-types are well scoped. Note the constructors and , which respectively represent type variables and their dual, and the quantifiers and which increase the number of quantifiers in the scoped pre-type. The dual of a pre-type is computed by the following function: It is straightforward to prove that duality is an involution. This property is important in the rest of the formalisation so we define an implicit rewriting rule that Agda can autonomously apply whenever possible. This is achieved by means of the following pragma directive.Footnote 1 Next we define the function that simultaneously substitutes the type variables of a pre-type with other pre-types. In practice we will always substitute one variable at a time, but it is technically easier to define so that it accepts a function substituting all variables of a pre-type, possibly with themselves. The definition of relies on some auxiliary functions for renaming type variables and lifting substitutions across quantifiers. These functions are straightforward adaptations of those described by [28]. Among all substitutions, we will use the one that substitutes the 0-indexed type variable with a pre-type. It is convenient to introduce this substitution once and for all, which we do here. Duality and substitutions are meant to commute. It is worth looking at one case in the proof of , namely when the type is a dualised type variable: Here we are supposed to prove which is definitionally equal to . We could easily prove this equivalence by invoking , but thanks to the rewriting rule that we have added earlier a use of suffices. In this case the saved effort is negligible, but in later results, where it is necessary to use for rewriting part of the index of some type families, having an implicit rewriting rule allows us to avoid writing some quite obscure Agda code. Just like too is key in the formalisation that follows. Therefore, we add it to the set of implicit rewriting rules used by Agda so that we do not have to think about this property again. We call closed pre-types, those having no free type variables. From now on, we will seldom use pre-types again. 3.2 Context Representation We are going to adopt a nameless representation of channels. Hence, typing contexts are represented as lists of types, where the (polymorphic) type and its constructors and are defined in the module of Agda’s standard library. We will keep using \(\Upgamma \), \(\Updelta \) and \(\Uptheta \) to range over typing contexts, even though in the Agda formalisation they are lists and not finite maps as in Sect. 2.4. The most important operation concerning typing contexts is splitting. The splitting of \(\Upgamma \) into \(\Updelta \) and \(\Uptheta \), which we denote by \(\Upgamma \simeq \Updelta + \Uptheta \), represents the fact that \(\Upgamma \) contains all the types contained in \(\Updelta \) and \(\Uptheta \), preserving both their overall multiplicity and also their relative order within \(\Updelta \) and \(\Uptheta \). A proof of \(\Upgamma \simeq \Updelta + \Uptheta \) shows how the types in \(\Upgamma \) are distributed in \(\Updelta \) and \(\Uptheta \) from left to right. When splitting a context \(\Upgamma \) into \(\Updelta + \Uptheta \), for each type in \(\Upgamma \) we use one of the prefix operators and to indicate whether the type is meant to be placed in \(\Updelta \) or in \(\Uptheta \). Once we reach the end of the typing context, we use the constructor to build the trivial splitting of the empty context into two empty partitions. For example, below is a proof of the splitting \([A, B, C, D] \simeq [B] + [A, C, D]\). It is easy to see that splitting is commutative and that the empty context/list is both a left and right unit of splitting. Context splitting is also associative. If we write \(\Updelta + \Uptheta \) for some \(\Upgamma \) such that \(\Upgamma \simeq \Updelta + \Uptheta \), then we can prove that \(\Upgamma _1 + (\Upgamma _2 + \Upgamma _3) = (\Upgamma _1 + \Upgamma _2) + \Upgamma _3\). When proving a splitting \(\Upgamma \simeq [A] + \Uptheta \) where the left partition is a singleton [A], it may be convenient to use as a shortcut for a sequence of applications of once the A type has been reached in \(\Upgamma \). For instance, can be written equivalently and in a more compact way as shown below. More usages of will be provided in Sect. 3.9. From now on we will make extensive use of predicates over contexts. For this reason, it is worth recalling in Table 4 a number of definitions from the module of Agda’s standard library. We begin using these definitions for building a few abstractions inspired by separation logic [31] that allow us to hide context splittings, at least in some cases. Following [35], we define the separating conjunction \(P \mathbin *Q\) of two predicates P and Q over contexts: If P and Q are predicates over contexts, the predicate \(P \mathbin *Q\) holds for those contexts \(\Upgamma \) that can be split into \(\Updelta \) and \(\Uptheta \) so that P holds for \(\Updelta \) and Q holds for \(\Uptheta \). The constructor has three explicit arguments witnessing the splitting \(\Upgamma \simeq \Updelta + \Uptheta \) along with proofs of \(P~\Updelta \) and \(Q~\Uptheta \). The use of metavariables P and Q for denoting predicates over contexts is appropriate: as we will see shortly, in our formalisation processes are indeed an example of predicate over typing contexts. Along with we define the separating implication (also known as “magic wand”) and prove that can be used to curry : To conclude the implementation of typing contexts, we define a predicate that holds for unrestricted contexts, those solely made of types of the form ?A. We need this predicate in the definition of a server, which must comply with the typing rule \([!]\). The empty context is trivially unrestricted. A non-empty context is unrestricted if its head has the form ?A for some A and its tail is unrestricted as well. It is easy to prove that \(\Upgamma \) is unrestricted if so are \(\Updelta \) and \(\Uptheta \) when \(\Upgamma \simeq \Updelta + \Uptheta \): 3.3 Context Permutations According to our nameless representation of channels, the position of a type in a typing context \(\Upgamma \) determines the location of its binder in the structure of a process. When the binding structure of a process changes, e.g. because a structural pre-congruence rule is applied, or when a channel substitution occurs, cf. the right-hand side of the [ax] reduction in Table 2, \(\Upgamma \) must be suitably rearranged to agree with the updated binding structure. Such rearrangement is in fact a permutation of the elements of \(\Upgamma \). We define typing context permutations inductively, as a binary relation : Each constructor of represents a particular kind of permutation: for the trivial permutation that does not change anything; for the permutation that swaps the first two elements of a typing context; for the permutation applied to the tail of a typing context; for the sequential composition of permutations. The definition of the data type is nearly the same found in the module of Agda’s standard library. We have preferred defining our own notion of permutation for simplicity and convenience: the constructor does not need a sub-permutation for the tail of the typing context, which can always be performed, if needed, combining with and . Also, and more importantly, our data type is monomorphic (it does not need to relate arbitrary lists) and the arguments A and B of and are implicit, which streamlines the usage of these constructors in the rest of the code. It is easy to see that is an equivalence relation. In the following we also use another property of permutations related to context splitting and list concatenation : if \(\Upgamma \simeq \Updelta + \Uptheta \), then \(\Upgamma \) is a permutation of the concatenation of \(\Updelta \) and \(\Uptheta \). 3.4 Channel and Process Representation We adopt an intrinsically-typed representation of processes with nameless channels. The intrinsically-typed representation makes sure that only well-typed processes can be constructed. This choice increases the effort in the definition of the datatypes for representing processes and their operational semantics, but pays off in the rest of the formalisation for at least three reasons: - we need not give explicit names to channels, thus we avoid all the technicalities and pitfalls that a named representation entails; - we conflate processes and typing rules in the same datatype, thus reducing the overall number of datatypes defined in the formalisation; - the typing preservation results are embedded in the very definition of the operational semantics of processes and do not require separate proofs (Sects. 3.5 and 3.6). Channels are not given any name. Instead, they are represented as terms witnessing that their type is present in the typing context. This is known as co-de Bruijn syntax [30], whereby the typing context associated with a term (a process, a channel) only contains the types of the channels that actually occur within the term. For this reason, typing contexts are split eagerly, according to the structure of processes, to make sure that channels are appropriately (and above all linearly) distributed among sub-processes, so that each channel is used exactly once. Concretely, a channel of type A is a predicate that holds for the singleton context : A process that is well typed in a typing context \(\Upgamma \) is a predicate that holds for \(\Upgamma \). Here is the datatype for representing processes: The constructor builds a link \(x\leftrightarrow y\). This process is well typed in a context of the form \(x: A, y: A^{\bot }\), namely a context satisfying the predicate which we see on the left-hand side of . The constructor builds a cut \((x:A)({P}|{Q})\). This process is well typed in a context \(\Upgamma \) if \(\Upgamma \simeq \Updelta + \Uptheta \) so that P and Q are well typed in the contexts \(x: A, \Updelta \) and \(x: A^{\bot }, \Uptheta \), which are obtained from \(\Updelta \) and \(\Uptheta \) by adding the bindings x : A and \(x: A^{\bot }\), respectively. Since x is the most recently introduced channel, the types A and \(A^{\bot }\) are added in front of \(\Updelta \) and \(\Uptheta \), which we do by means of the functions and . These are partial applications of the constructor for lists to which we have supplied the left operand. All the remaining constructors basically follow the same pattern: they possibly quantify over some types A and B and then (implicitly) over a typing context \(\Upgamma \) through the function applied to a predicate of the form . The predicate states how to build a process that is well typed in \(\Upgamma \), provided that \(\Upgamma \) satisfies P. In general, P is a (separating) conjunction of sub-predicates corresponding to the channel on which the process is acting and to the premises of its typing rule. For example, the constructor , which builds a process \(x \triangleright \{\}\), requires the context \(\Upgamma \) to satisfy the predicate , meaning that \(\Upgamma \) must contain an entry ( is the universal predicate that holds for every context, cf. Table 4). That form of \(\Upgamma \) matches the typing context in the conclusion of the rule \([\top ]\). The constructor , which builds a process \(x().P\), requires \(\Upgamma \) to (separately) satisfy , that is the channel x on which the process is operating, as well as , that is the continuation process P, which must be well typed in the remaining typing context. The constructor , which builds a process \(x[]\), requires the typing context to be the singleton list \([\textbf{1}]\). Let us move on to the forms that produce continuation channels. As an example, the constructor builds a process , where both P and Q use the continuation channel y. In this case \(\Upgamma \) must satisfy the predicate which looks intimidating at first but makes perfect sense once we recall the typing rule \( [{ \& }]\)and the definitions of and in Table 4. Remember that we are trying to establish whether is well typed in \(\Upgamma \). The predicate expresses the requirement that the type of x must be of the form \( A { \& }B\) and should be found in \(\Upgamma \). In other words, \( \Upgamma \simeq [A { \& }B] + \Updelta \) for some \(\Updelta \). Now P and Q must be well typed in the context \(\Updelta \) augmented with the association y : A and y : B, respectively, whence the use of to verify a (non-separating) conjunction of the predicates and . The two new contexts are obtained by adding either A or B to \(\Updelta \), which we perform using . Crucially, the types A and B are prepended to \(\Updelta \), which is consistent with the fact that the continuation y has been freshly introduced and the channel x has been consumed. Notice how easy it is to prepend either A or B to \(\Updelta \) instead of changing the type of x in \(\Upgamma \) from \( A { \& }B\) to either A or B while preserving the position of the type, as we would have to do in a “true” session type system without explicit continuation channels. The interpretation of the remaining constructors is analogous, so we only comment , which builds a process \(x(X,y).P\). This constructor models the continuation P using higher-order abstract syntax (HOAS): proving that a context \(\Upgamma \) satisfies the predicate means providing a function that, for every type X, produces a witness for the predicate applied to \(\Upgamma \). Note that the side condition \(X \not \in \textsf{fv}(\Upgamma )\) of \([\forall ]\)is trivially enforced by definition: A has type , that is a pre-type with at most one free type variable X, whereas \(\Upgamma \) is a typing context, that is a list of without free type variables. Therefore, X cannot occur in \(\Upgamma \). We conclude this module by proving that permutations preserve process typing. Since list permutations basically correspond to channel renaming, we can read this property as the fact that typing is preserved by (bijective) name substitutions. 3.5 Structural Pre-congruence We formalise structural precongruence as a binary relation between processes that are well typed in the same typing context. This entails that structural precongruence preserves typing by definition. The datatype for \(\sqsupseteq \) has one constructor for each structural pre-congruence rule in Table 2. Since many aspects recur repeatedly, we illustrate the implementation of just a few representative rules starting from [s-comm]. The constructor models the commutativity property of parallel composition. We use to compute the proof of the splitting \(\Upgamma \simeq \Upgamma _2 + \Upgamma _1\) from p. Notice that makes key use of the implicit rewriting rule described in Sect. 3.1. Indeed P and Q have type and , respectively, but the on the r.h.s. of expects P to have type . Thanks to , Agda considers these types equivalent without requiring intricate substitutions in the index of . The constructor models the [s-wait] rule: There are two non-trivial aspects worth commenting. The first one concerns the proof used within . To understand the meaning of this proof, we must recall three key elements: - (1) is a direct sub-process of the , and therefore it is meant to be well typed in the context . - (2) Being a process, such context must contain a \(\bot \) type as per the typing rule \([\bot ]\). That is for some \(\Updelta \). - (3) The [s-wait] rule is applicable only provided that the channel restricted by the cut (say x, of type A) is different from the channel consumed by the process (say y, of type \(\bot \)). We enforce the side condition \(x \ne y\) of [s-wait] (which we left implicit in Table 2) imposing that the type A in front of goes to the right partition of the splitting through the use of . The other aspect that is worth commenting concerns the rearrangement of the splittings in the process after the application of structural precongruence. Overall, p and q prove the splittings \(([\bot ] + \Updelta ) + \Upgamma _2\), but the precongruence rule requires this splitting to be rearranged as \([\bot ] + (\Updelta + \Upgamma _2)\). That is, we need to apply the left-to-right associativity property of context splitting which we called in Sect. 3.2. The nested allows us to pattern match on the result of the application and to extract the new proofs \(p'\) and \(q'\) for the rearranged splittings. The constructors and model [s-select] when the selected tag is respectively and . For example, for we have: Here the process , that is , is found under a cut for x : A and is using some channel \(y: B \oplus C\) to select . The continuation process P uses a fresh continuation channel z : B. Therefore, P is required to be well typed in the context , where the type B of z comes before the type A of x since z is introduced later than x. After structural pre-congruence is applied, however, the type of the continuation channel z ends up behind that of the restricted channel x, because now z and x are introduced in the opposite order. Therefore, we need to rename the channels in P so that it is well typed in the context . Such renaming is achieved applying the function to the permutation and to the process P. We also discuss the modeling of the [s-fork-l] rule, which is interesting because of its complex side conditions: Recall from Table 2 that we allow using this rule on a process of the form when \(x \in \textsf{fc}(P)\). We capture the condition \(x\in \textsf{fc}(P)\) by means of the splitting , implying that the type A of x ends up in the typing context for P and not in the one for Q. The symmetric rule [s-fork-r] is modeled by another constructor , which is similar to except that is replaced by . Finally, in Sect. 2.3 we have colloquially defined \(\sqsupseteq \) as a “pre-congruence”, implying that it is a reflexive, transitive relation preserved by some forms of the calculus. In the formalisation we have to be precise and we introduce specific rules: Note that we define a single congruence rule that allows us to apply \(\sqsupseteq \) within cuts, but not underneath prefixes. This limited form of pre-congruence turns out to be sufficient for the development that follows. We concede that the implementation of the pre-congruence rules (including those not discussed here) can be difficult to decipher. In part, this is due to the fact that splitting proofs are manifest and no longer hidden by separating conjunctions (as in Sect. 3.4) because we need them to enforce the side conditions of the rules in Table 2. We should also bear in mind that, using an intrinsically-typed representation of processes, we have already taken care of the proof that structural pre-congruence preserves typing. 3.6 Reduction Just like structural pre-congruence, reduction is formalised as a binary relation between processes that are well typed in the same typing context. Thus, the definition of reduction embeds subject reduction (Theorem 2.1). There is a constructor for each of the reduction rules in Table 2. Let us comment on a few representative cases. The constructor models the reduction \((x:A)({x\leftrightarrow y}|{P}) \leadsto P\{y/x\}\) called [r-link] in Table 2: The splitting p indicates that y (of type \(A^{\bot }\)) occurs in the left sub-process of the cut (that is the link \(x\leftrightarrow y\)) and the splitting to which is applied is structured consistently with the syntax of the link being reduced, which is oriented so that the restricted channel x is on the left. The process P has type and turns into \(P\{y/x\}\) after the reduction. The type of x in P is the first in the typing context, indicating that it is the newest channel that P is aware of; however, after the reduction, x is replaced by y which is found somewhere within \(\Upgamma \). The exact location of y in \(\Upgamma \) is encoded in the splitting p, thus we “rename” x into y within P using the permutation . The constructor models [r-close]: While the process constructor implicitly refers to the only free channel occurring in a process of the form \(x[]\), the constructor uses a splitting proof of the form to make sure that the referenced channel is also the restricted one, and therefore matches the one of the process. Note that (and several other reduction constructors) quantifies over \(p_0\) and \(q_0\) which both prove the splitting . Since the left partition is empty, these splittings must be equal and made of a sequence of applications followed by . In general, Agda will not be able to “see” that they are definitionally equal, hence it is easier to quantify over them separately so that we do not have to prove their equality whenever we wish to apply this reduction. The constructor models [r-select] when the selected tag is : There is not much to note here except again for the multiple quantifications over the trivial splittings and the use of to make sure that the channel referred to by and is indeed the one restricted by the cut. The remaining constructors that describe the base reductions follow a similar pattern, except for the implementation of [r-weaken] and [r-contract] which require auxiliary functions to respectively weaken and contract the typing context of the resulting process as shown in Table 2. It is worth glancing at the implementation of [r-exists] since it involves a non-trivial rewriting of types: Recalling the definitions of and from Sect. 3.4, we note that P has type and F B is a process of type . In order for these two processes to be composable in a cut, it must be the case that , which was proved in Sect. 3.1 under the name . Thanks to the implicit rewriting rule, we do not have to rewrite the index in the type of F B, which is silently accepted as is. Reduction is closed under cuts and by structural pre-congruence as per [r-cut] and [r-cong]. The corresponding constructors that model these features are shown below: 3.7 Deadlock Freedom As we have seen in Sect. 2, the deadlock freedom property and Theorem 2.2 rest on some notions and predicates about processes which must be formalised in Agda. First of all we need to define the notion of thread, that is any process other than a cut. It is convenient to provide a more fine-grained classification of threads, distinguishing between links and input/output actions and sometimes also on whether such actions operate on free or bound channels. We define predicates for each of these classes: The implementation of these predicates is not interesting since it is essentially isomorphic to the relevant fragments of the datatype. The only aspect that is worth pointing out here is that in , and the channel being acted upon by the thread is the first in \(\Upgamma \), hence it is the most recently introduced channel, whereas in and the channel is not the first. This allows us to distinguish those threads that, in the context of a cut, operate on the channel bound by the cut or on a free channel. To clarify this aspect, let us look at the implementation of the constructor in and in . In the former predicate we have where the use of the constructor indicates that the thread operates on the most recent channel. In the latter predicate we have where the use of the constructor indicates that the thread operates on a channel other than the most recent one. Note that here we have to specify the type C in front of \(\Upgamma \) or else Agda is unable to automatically resolve some metavariables. The predicate is simply the disjoint union of all the previous ones. Observability, reducibility and aliveness are straightforward formalisations of their pen-and-paper version: In order to prove that every (well-typed) process is alive, it is convenient to define a “canonical” form for cuts, that is a form that matches at least one of the l.h.s. of one of the rules for structural pre-congruence or reduction in Table 2. This is the point where the fine-grained classification of threads introduced earlier pays off: instead of considering all the 21 forms of cuts that can be rewritten/reduced according to the rules in Table 2, we only need to consider four major classes of cuts: A canonical cut \((x:A)({P}|{Q})\) has one of these forms: - P is a link ( ), or - P performs an output on x and Q performs an input on x ( ), or - P operates on a channel other than x and is not a server ( ), or - both P and Q are servers and P operates on a channel other than x ( ). Note that we have to distinguish servers from the other input operations because the structural pre-congruence rule [s-server] can only be applied when the two sub-processes of a cut are both servers. Every cut \((x:A)({P}|{Q})\) where both P and Q are threads can be rewritten into a canonical cut using structural pre-congruence: It is easy to prove that every canonical cut is alive, either reducing it or applying structural pre-congruence to rewrite it into a thread. Now deadlock freedom for P can be proved by induction on P. When P is a thread, then it is obviously observable and hence alive. When P is a cut \((x:A)({P}|{Q})\), is applied recursively to P and to Q, in turn. If either of these applications yields a reduction, then the whole cut is reducible and therefore alive. If both applications yield a thread, then we conclude that the cut is alive first rewriting it into a canonical cut with and then using . 3.8 Type Safety We have seen that type safety is a simple instance of deadlock freedom, which is made even simpler to formalise in our development where processes are intrinsically typed. We start by defining reduction contexts as processes with a single hole. In our intrinsically-typed formalisation, reduction contexts are parameterised by the typing context \(\Updelta \) of the hole, which is invariant, and indexed by the typing context \(\Upgamma \) of the whole reduction context: The constructor builds a hole, as the name implies. The constructors and build reduction contexts where the hole is found in the left (respectively, right) sub-term of a cut, as per the grammar of reduction contexts given in Sect. 2.5. Substitution inside a reduction context \(\mathcal {C}\) is a straightforward function that operates recursively on the structure of \(\mathcal {C}\): This notion of process substitution preserves typing by construction thanks to the fact that both processes and reduction contexts are intrinsically typed. A process P is well formed if every unguarded sub-process Q in it is alive. The proof of type safety ends up being a trivial application of . No work is needed to deduce that the process Q in the hole of a reduction context is well typed because structural pre-congruence preserves typing by definition. 3.9 Examples In this section we revisit and expand the processes discussed in Examples 2.1 and 2.3 and show their encoding in our formalisation. The encoding of \(\mathbb {B}\) is straightforward We take advantage of the host language for programming higher-order processes. For example, we can define a conditional process thus: A term is a process that waits for a boolean value (cf. the type at the front of its typing context) and continues as either P or Q depending on whether it receives true or false. We use (defined in Sect. 3.2) to curry the constructor so that we can supply its arguments one by one saving a few parentheses and reducing clutter (more on this in Remark 3.1 at the end of this section). Next we define a process that consumes a boolean and continues as P regardless of its value. Using these higher-order forms, it is easy to define the usual boolean connectives. The function (defined in Agda’s standard library) is just a low-precedence, visible function application operator. We use it as a separator to flatten deeply nested expressions and save a bunch of parentheses. For the sake of illustration, we have chosen to define the disjunction from the conjunction and negation using De Morgan’s laws. To test our definitions, we implement a simple evaluator using the deadlock freedom property. We have not proved a termination result, but since linear logic enjoys cut elimination we can safely annotate the evaluator as terminating. Now if we ask Agda to normalise the goal we obtain , that is the definition of , as expected. For the encoding of the polymorphic echo server (Example 2.3), we start by encoding its type \(!(\forall X.X^{\bot }\bindnasrepma (X \otimes \textbf{1}))\): The notation (defined in Agda’s standard library) creates an element of from the natural number n. Here it is used to create the de Bruijn index of the type variable X. We now encode the server and the client that sends true to it To test our definitions, we compose client and server in parallel and then ask Agda to normalize , which yields as expected. Remark 3.1 Writing processes in Agda would be more pleasant if the constructors of the data type were naturally curried, instead of currying them on demand with as we do here. Below is the naturally curried constructor of a hypothetical data type , obtained by expanding the definition of separating conjunction: This version of is fully curried, but also less readable than the one we gave in Sect. 3.4 because of the (now visible) context splittings. We can recover some clarity and still obtain a curried version of using (literally) the magic wand: However, the first arrow must be a plain implication and not a magic wand to account for the appropriate amount of context splittings. We think that this formulation of the constructors would be harder to explain and motivate in the context of Sect. 3.4. Since none of the alternative definitions of was fully satisfactory, we preferred the most elegant version of the data type at the expense of additional clutter in this section. \(\lrcorner \) 4 On the Equivalence of LCC and CP In Sect. 1 we have anticipated that LCC is a “linear version” of CP in which sessions are encoded instead of being featured natively. In this section we substantiate this claim by sketching a straightforward isomorphism between (well-typed) CP processes and (well-typed) LCC processes, up to bound names. Such tight correspondence can be traced back to the papers by Kobayashi [26] and Dardha et al. [11] showing how (binary) sessions can be encoded as chains of linear channels. In the rest of this section, we detail this correspondence focusing on the multiplicative/additive connectives. The treatment of quantifiers is similar, and the other parts of LCC coincide with those of CP. To avoid ambiguity, we use \(\textsf{P}\) and \(\textsf{Q}\) (in sans-serif font) to range over CP processes and we write \(\textsf{P}\vdash _{\textsc {cp}}\Upgamma \) for a CP typing judgment. In CP, the process forms representing input/output operations on sessions are \(x(y).\textsf{P}\) and (for inputs) and \(x[y](\textsf{P}|\textsf{Q})\) and (for outputs). The key difference between these forms and the corresponding ones in LCC is the absence of an explicit continuation channel. Instead, as we have seen in Example 2.1, the session endpoint x is being used by the continuation processes \(\textsf{P}\) and \(\textsf{Q}\) to implement the rest of the session. This is made clear by the CP typing rules for these processes, which we recall below [40]: Every (well-typed) CP process can be encoded into a (well-typed) LCC process by introducing an explicit continuation channel that does not clash with other channel names. In order to express such encoding easily as a function \(\varepsilon (\cdot )\), following Sano et al. [36] we pick as the name of the continuation channel the very same name of the session that it continues. The encoding function is defined by the following equations and extended homomorphically to the other forms of CP. Every (well-typed) LCC process can be decoded into a (well-typed) CP process by renaming each continuation channel so that it matches the name of the session it continues. The decoding function \(\delta (\cdot )\) is defined by the following equations and extended homomorphically to the other forms of LCC. It is now easy to establish that \(\varepsilon (\cdot )\) and \(\delta (\cdot )\) are inverses of each other (up to alpha conversion) and that they preserve typing, in the sense that: - If \(\textsf{P}\vdash _{\textsc {cp}}\Upgamma \), then \(\varepsilon (\textsf{P})\vdash \Upgamma \); - If \({P}\vdash \Upgamma \), then \({\delta (P)}\vdash _{\textsc {cp}}\Upgamma \). Note that an LCC process P and its decoding \(\delta (P)\) (or equivalently a CP process \(\textsf{P}\) and its encoding \(\varepsilon (\textsf{P})\)) are typed in the same typing context (up to the name of channels, for typing judgments other than the concluding one). 5 Related Work We have compared our formalisation with others of typed calculi that support binary sessions either natively or through their encoding using continuations [26, 27]. Goto et al. [16] describes the formalisation of a session-based variant of the \(\pi \)-calculus which supports channel polymorphism. This is the oldest formalisation of a session-based calculus for which we were able to retrieve the source code (the work of [12] predates this one, but its source code is not publicly available any more). Thiemann [37] formalises a subset of GV [14], a functional language extended with session communication primitives, along with an interpreter. Ciccone and Padovani [10] have taken inspiration from his work to formalise a variant of the linear \(\pi \)-calculus [27] that supports dependent types, so as to enable the description of communication protocols whose structure may depend on the content of messages. Castro-Perez et al. [7] describe EMTST, a library for the formalisation of session-typed systems that includes as case studies the session calculus of [18] (called “original system”) and a revised version of it that is more amenable to be formalised using a locally nameless representation of channels. Rouvoet et al. [35] present a library of abstractions inspired by separation logic, aiding the formalisation of interpreters for languages with linear resources. One of the presented case studies is the formalisation of a fragment of GV [14, 40]. Unlike the other formalisations we are discussing, Rouvoet et al. [35] do not define a small-step semantics for GV but their formalisation is intrinsically typed, hence the interpreter proves a form of subject reduction property. The separating conjunction defined in Sect. 3.2 and the typing of the constructors for the representation of processes in Sect. 3.4 have been adapted from this work of [35]. Jacobs et al. [22] formalise a library of connectivity graphs for reasoning on and enforcing deadlock freedom in a variant of GV [14, 40]. This is the first formalisation of deadlock freedom for a calculus of sessions. All the formalisations mentioned so far make use of context splitting. In contrast, Zalakain and Dardha [43] formalise a generalisation of the linear \(\pi \)-calculus which is parametric in a usage algebra (to account for channel sharing/linearity) and is based on leftover typing [2]. Typing judgments have the form \(\Upgamma \vdash P \vartriangleright \Updelta \) so that a process P is typed with respect to an input context \(\Upgamma \), which describes all the available channels, and a context of leftovers \(\Updelta \), which describes the residual channels not consumed by the process. In this way, it is possible to “concatenate” typing judgments by matching the leftovers in one judgment with the input context of the subsequent one, with no need for splitting. As [43] nicely summarise, context splittings are not necessary because they “contain usage information that is already present in processes.” This is true provided that channels are named (Zalakain and Dardha [43] use de Bruijn indices to this aim). In fact, the co-de Bruijn representation of processes [30], whereby channels are nameless and context splitting is performed eagerly, can be seen as the “dual approach” of leftover typing: channel names provide information that is already present in their (singleton) typing context, hence they can be omitted from contexts and processes. Motivated by the technical difficulties arising from context splittings, Sano et al. [36] define a structural version of CP using an approach based on linearity predicates. The key idea is to treat typing contexts structurally and to enforce the linear usage of channels by checking their syntactical occurrence in processes. Interestingly, this approach relies on the explicit naming of continuations so as to precisely account for the number of times a channel is actually used. Sano et al. [36] do not connect their technique with the continuation-passing encoding of binary sessions [11, 26], but the analogies are evident even though the role of continuations differs. In particular, SCP continuations are new names given to existing channels to enable the distinction between multiple occurrences of the same (session) channel. In contrast, LCC continuations are new channels used to encode the session as a chain of linear channels [11, 26]. Zackon et al. [42] describe a typing context management technique where channels are associated not just with a type but also with a tag, that is an element of a given resource algebra that summarises the number of allowed usages of a particular channel, including the possibility that the channel is not available. This approach streamlines context splitting since contexts can be treated in an essentially structural way, except for tags which are conveninently combined using operations from the resource algebra. Table 5 shows an overview of the aforementioned formalisations (sorted by publication date) including our own. The first five columns identify the calculus being formalised. We provide its reference paper, the prover in which it is formalised and an acronym that gives an idea of the flavour of the calculus. We also specify whether the calculus features cuts (that is, the combination of restriction and parallel composition corresponding to the cut of linear logic) and continuations. CP [15, 40] and GV [14, 40] are well-known acronyms in the literature on session types. \(\textsf {S}\pi \) refers to (variants of) the session-based \(\pi \)-calculus presented by [18] while L \(\pi \) refers to (variants of) the linear \(\pi \)-calculus [27]. Finally, SCP is the structural version of CP introduced by [36] and LCC is our calculus. We emphasize that the actual calculus being formalised usually differs from (typically, is a strict subset of) the one identified by the acronym and that the same acronym may sometimes refer to different versions of the same calculus. In particular, GV in a logical setting is described by [40] but its first (non-logical) version is due to [14]. Concerning the use of continuations, the approaches based directly on the linear \(\pi \)-calculus (into which sessions can be encoded) are marked with + and those based on a calculus with native sessions are marked with −. The calculus SCP is marked with ± because, while not directly inspired to the linear \(\pi \)-calculus, it makes use of explicit continuations for defining the predicates that check the linear usage of channels. Finally, all the approaches based on GV are also marked with ±. Officially, none of these calculi makes use of continuations, but GV is designed in such a way that each operation acting on a channel s is a function that returns the result of the operation (if present) along with the same channel s. In this way, the type of s can be conveniently “updated” to take into account the effect of the operation. As observed by [33], this semantics of the communication primitives is virtually indistinguishable from one making use of explicit continuation channels. The three middle columns of Table 5 report the relevant qualitative aspects of the formalisations, namely the management of typing contexts, the representation of channels and whether processes are intrinsically or extrinsically typed. The rightmost columns report the size (in kilobytes) of the formalisations as rough (and possibly questionable) estimates of their complexity. Papers describing formalisations typically report the “lines of code” as a measure of development effort, but the number of lines may be affected by code indentation styles and syntactical constraints of the proof assistant being used. For this reason, we have preferred to count the total number of characters after comments have been removed and spaces have been squeezed.Footnote 2 The reported sizes account for the source code of the formalisations excluding examples and any safety result, if present. We have excluded safety results because their meaning varies widely across the formalisations and, except for our own, they all differ from the one stated in the linearity challenge [6]. Some formalisations [22, 35, 42, 43] define libraries which can be reused in different contexts. In these cases, the size of the library is reported separately next to the size of the part of the development that uses it. In general, it is difficult to draw firm conclusions on the effectiveness of the various approaches in addressing the linearity challenge because the formalisations differ widely for a variety of entangled factors. Looking at the available data, we can make the following observations. The adoption of context splitting, which is very well represented, does not seem to be a good indicator of the complexity of the formalisation. Indeed, the formalisations based on context splitting span the whole range of sizes, from the largest by [16] (543 kb) to our own (21 kb, without the proof of deadlock freedom) which is also the only one supporting all the features of CP. The two largest formalisations [7, 16] are also the ones that adopt a locally nameless representation of channels. In these formalisations channels are represented in two different ways, depending on whether they are free or bound. This entails some duplication of effort as well as some transformation machinery between the two representations. Other channel representations are not strong complexity indicators. Note that the adoption of co-de Bruijn syntax implies the use of context splitting, hence the two aspects are not completely independent. There is no strong evidence that the intrinsically typed representation of processes reduces the size of the formalisation. As observed in Sect. 3.4, this choice helps reducing the overall number of datatypes to be defined and makes some results trivial (e.g. Theorem 2.3 formalised by ), but the definitions are also more involved because they incorporate invariants and bits of the proofs of typing preservation. We speculate that the effort for representing processes, types and typing rules is not substantially impacted overall, but the data types for representing syntax and semantics of untyped processes in extrinsically-typed representations are certainly more readable. Using the cut in the style of linear logic instead of separate restriction and parallel composition simplifies the representation of channels (or session endpoints). All the formalisations of calculi that adopt the cut tend to be small (if we exclude the libraries), but this is not a general rule. Finally, it appears that the use of (explicit) continuations is related to the complexity of the formalisation more than anything else. Indeed, the six smallest formalisations (excluding the deadlock freedom results)—with an average size of around 62 kb—are all based on continuations, no matter if they are explicit (L \(\pi \), SCP, LCC) or “virtual” (GV), while the remaining ones are 263 kb on average. At the very least, the use of continuations enables a cleaner management of typing contexts since linear channels are true “use-once” resources, and there is no need to update their type. There is a rich literature documenting formalisations of (fragments of) linear logic in various proof assistants [2, 8, 9, 25, 34, 41]. In these papers, the focus is on the properties of the logic itself rather than its interpretation as a model of concurrency. Kalvala and de Paiva [25] and Power and Webster [34] explore the problem of interactive proof search in Isabelle and Coq, respectively. Chaudhuri et al. [8, 9] and Xavier et al. [41] formalise some meta-theory of sequent calculi for linear logic, in particular cut elimination and the completeness of focusing. In these papers, contexts are represented either as lists of propositions (with explicit exchange rules) or as multisets (lists up to permutations). The latter representation is essentially the same as what we adopt in this paper, although in our case the position of a type/proposition in a typing context implicitly carries the binding information of the channel it corresponds to. Allais [2] introduces the technique of leftovers to develop an Agda formalisation of intuitionistic multiplicative-additive linear logic. Sequents have both an input context (the overall available resources) and an output context (the leftovers, or resources that have not been consumed), so as to avoid the problem of context splitting altogether. The leftovers technique has subsequently inspired the formalisation of the linear \(\pi \)-calculus by Zalakain and Dardha [43]. In this work, following [35], we have used some key concepts of separation logic, namely separating conjunction and the magic wand, as tools to streamline the representation of processes. Separation logic has also been used to develop standalone formal verification frameworks for concurrent programs. In particular, Actris [17] and LinearActris [24] allow the verification of functional properties of programs that mix-and-match various concurrency abstractions including shared/mutable state, locks and communication channels regulated by session types. 6 Concluding Remarks We have presented a formalisation of LCC, a linear calculus of continuations closely related to the linear \(\pi \)-calculus [27] and supported by the same type system as CP [40]. Binary sessions can be modeled in LCC using the continuation-passing encoding described by [26, extended version] and [11]. The linear calculus of continuations and the calculus described in the linearity challenge [6] are incomparable in terms of expressiveness. On the one hand, the challenge only considers a minimal calculus of first-order, monomorphic sessions while LCC supports linear, shared, higher-order, polymorphic channels; on the other hand, the calculus of the challenge allows the modeling of sequential processes owning both endpoints of a session and in general of cyclic network topologies, none of which can be modeled in LCC because of its tight correspondence with linear logic. We think that LCC deserves its own space in the context of the linearity challenge alongside with (but not in substitution of) more traditional session calculi. Considering the richness of LCC in terms of features and proved properties, the simple formalisation of LCC casts some doubts on the actual role of context splitting as a source of complexity. We perceive more tangible benefits from the adoption of a calculus with explicit continuations where channels are linear in a literal sense. In this respect, we find it intriguing that, among the alternative approaches that have been proposed to overcome the difficulties of context splitting, the one by [36] makes key use of explicit continuations. The compact formalisation we have presented is very much tailored to the specific features of LCC and, in our opinion, it is hardly reusable in substantially different contexts. However, it is a good starting point for further developments of the LCC calculus. In fact, we have already extended LCC with support for coinductive (i.e. possibly infinite) types, recursive processes and context-free session types (these extensions are in LCC ’s public repository [32]). At the level of the syntax and of the typing rules, the extension of LCC with the so-called mix rule, which allows the parallel composition of independent processes not sharing any channel, is straightforward. However, this extension might require non-trivial changes to the definition and formalisation of deadlock freedom (Sect. 3.7) to handle some corner cases that are not contemplated in LCC as it stands. As an example, in a version of LCC with the mix rule, the process \(x[]\mathbin |y[]\) should be considered deadlock free even if it does not reduce and is not a thread. In the future, it would be interesting to formalise the strong normalisation property of LCC as a consequence of cut elimination of classical linear logic. In this work we have focused on models of binary sessions (those connecting exactly two processes), but there are also formalisations of multiparty sessions, notably those by [23, 38], which can be significantly more complex than those of binary sessions. The formalisation by [23] amounts to 173kb and the one by [38] to more than 1Mb of Coq code. Also in these cases, the formalisation based on (virtual) continuations [23] happens to be substantially smaller. Whether this is a coincidence or further evidence of the effectiveness of the continuation-based approaches is left for future investigations. Data Availability No datasets were generated or analysed during the current study. Notes The directive is effective provided that the option--rewriting is enabled, either globally when invoking Agda or within an pragma directive in the module’s source code. Sequences of two or more consecutive space-like characters are collapsed into a single space. The squeezing is obtained by running the command tr -s [:space:] file on Unix-like systems. References Abramsky, S.: Computational interpretations of linear logic. Theor. Comput. Sci. 111(1&2), 3–57 (1993). https://doi.org/10.1016/0304-3975(93)90181-R Allais, G.: Typing with leftovers—a mechanization of intuitionistic multiplicative-additive linear logic. In: Abel, A., Forsberg, F.N., Kaposi, A. (eds.) 23rd International Conference on Types for Proofs and Programs, TYPES 2017, Budapest, Hungary, 29 May–1 June2017. LIPIcs, vol. 104, pp. 1–1122. Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2017). https://doi.org/10.4230/LIPICS.TYPES.2017.1 Bellin, G., Scott, P.J.: On the pi-calculus and linear logic. Theor. Comput. Sci. 135(1), 11–65 (1994). https://doi.org/10.1016/0304-3975(94)00104-9 Caires, L., Pfenning, F.: Session types as intuitionistic linear propositions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010—Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, 31 August–3 September 2010. Proceedings. Lecture Notes in Computer Science, vol. 6269, pp. 222–236. Springer (2010). https://doi.org/10.1007/978-3-642-15375-4_16 Caires, L., Pfenning, F., Toninho, B.: Linear logic propositions as session types. Math. Struct. Comput. Sci. 26(3), 367–423 (2016). https://doi.org/10.1017/S0960129514000218 Carbone, M., Castro-Perez, D., Ferreira, F., Gheri, L., Jacobsen, F.K., Momigliano, A., Padovani, L., Scalas, A., Tirore, D.L., Vassor, M., Yoshida, N., Zackon, D.: The concurrent calculi formalisation benchmark. In: Castellani, I., Tiezzi, F. (eds.) Coordination Models and Languages—26th IFIP WG 6.1 International Conference, COORDINATION 2024, Held as Part of the 19th International Federated Conference on Distributed Computing Techniques, DisCoTec 2024, Groningen, The Netherlands, 17–21 June 2024, Proceedings. Lecture Notes in Computer Science, vol. 14676, pp. 149–158. Springer (2024). https://doi.org/10.1007/978-3-031-62697-5_9 Castro-Perez, D., Ferreira, F., Yoshida, N.: EMTST: engineering the meta-theory of session types. In: Biere, A., Parker, D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems—26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, 25–30 April 2020, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12079, pp. 278–285. Springer (2020). https://doi.org/10.1007/978-3-030-45237-7_17 Chaudhuri, K., Lima, L., Reis, G.: Formalized meta-theory of sequent calculi for substructural logics. In: Nigam, V., Florido, M. (eds.) 11th Workshop on Logical and Semantic Frameworks with Applications, LSFA 2016, Porto, Portugal, 1 January 2016. Electronic Notes in Theoretical Computer Science, pp. 57–73. Elsevier (2016). https://doi.org/10.1016/J.ENTCS.2017.04.005 Chaudhuri, K., Lima, L., Reis, G.: Formalized meta-theory of sequent calculi for linear logics. Theor. Comput. Sci. 781, 24–38 (2019). https://doi.org/10.1016/J.TCS.2019.02.023 Ciccone, L., Padovani, L.: A dependently typed linear \(\pi \)-calculus in Agda. In: PPDP ’20: 22nd International Symposium on Principles and Practice of Declarative Programming, Bologna, Italy, 9–10 September 2020, pp. 8–1814. ACM (2020). https://doi.org/10.1145/3414080.3414109 Dardha, O., Giachino, E., Sangiorgi, D.: Session types revisited. Inf. Comput. 256, 253–286 (2017). https://doi.org/10.1016/j.ic.2017.06.002 Gay, S.J.: A framework for the formalisation of pi calculus type systems in Isabelle/HOL. In: Boulton, R.J., Jackson, P.B. (eds.) Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, 3–6 September 2001, Proceedings. Lecture Notes in Computer Science, vol. 2152, pp. 217–232. Springer (2001). https://doi.org/10.1007/3-540-44755-5_16 Gay, S.J., Hole, M.: Subtyping for session types in the pi calculus. Acta Inform. 42(2–3), 191–225 (2005). https://doi.org/10.1007/S00236-005-0177-Z Gay, S.J., Vasconcelos, V.T.: Linear type theory for asynchronous session types. J. Funct. Program. 20(1), 19–50 (2010). https://doi.org/10.1017/S0956796809990268 Gay, S.J., Vasconcelos, V.T.: Session Types. Cambridge University Press, Cambridge (2025). https://doi.org/10.1017/9781009000062 Goto, M.A., Jagadeesan, R., Jeffrey, A., Pitcher, C., Riely, J.: An extensible approach to session polymorphism. Math. Struct. Comput. Sci. 26(3), 465–509 (2016). https://doi.org/10.1017/S0960129514000231 Hinrichsen, J.K., Bengtson, J., Krebbers, R.: Actris: session-type based reasoning in separation logic. Proc. ACM Program. Lang. 4(POPL), 6–1630 (2020). https://doi.org/10.1145/3371074 Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) Programming Languages and Systems—ESOP’98, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’98, Lisbon, Portugal, 28 March–4 April 1998, Proceedings. Lecture Notes in Computer Science, vol. 1381, pp. 122–138. Springer (1998).https://doi.org/10.1007/BFB0053567 Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR ’93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, 23–26 August 1993, Proceedings. Lecture Notes in Computer Science, vol. 715, pp. 509–523. Springer (1993). https://doi.org/10.1007/3-540-57208-2_35 Horne, R., Padovani, L.: A logical account of subtyping for session types. J. Log. Algebr. Methods Program. 141, 100986 (2024). https://doi.org/10.1016/J.JLAMP.2024.100986 Hüttel, H., Lanese, I., Vasconcelos, V.T., Caires, L., Carbone, M., Deniélou, P., Mostrous, D., Padovani, L., Ravara, A., Tuosto, E., Vieira, H.T., Zavattaro, G.: Foundations of session types and behavioural contracts. ACM Comput. Surv. 49(1), 3–1336 (2016). https://doi.org/10.1145/2873052 Jacobs, J., Balzer, S., Krebbers, R.: Connectivity graphs: a method for proving deadlock freedom based on separation logic. Proc. ACM Program. Lang. 6(POPL), 1–33 (2022). https://doi.org/10.1145/3498662 Jacobs, J., Balzer, S., Krebbers, R.: Multiparty GV: functional multiparty session types with certified deadlock freedom. Proc. ACM Program. Lang. 6(ICFP), 466–495 (2022). https://doi.org/10.1145/3547638 Jacobs, J., Hinrichsen, J.K., Krebbers, R.: Deadlock-free separation logic: linearity yields progress for dependent higher-order message passing. Proc. ACM Program. Lang. 8(POPL), 1385–1417 (2024). https://doi.org/10.1145/3632889 Kalvala, S., Paiva, V.: Mechanizing linear logic in Isabelle. In: Proceedings of the 10th International Congress of Logic, Philosophy and Methodology of Science, 1995 (1995) Kobayashi, N.: Type systems for concurrent programs. In: 10th Anniversary Colloquium of UNU/IIST. LNCS 2757, 2002, pp. 439–453. Springer (2002). Extended version available at http://www.kb.ecei.tohoku.ac.jp/~koba/papers/tutorial-type-extended.pdf Kobayashi, N., Pierce, B.C., Turner, D.N.: Linearity and the pi-calculus. ACM Trans. Program. Lang. Syst. 21(5), 914–947 (1999) Kokke, W., Siek, J.G., Wadler, P.: Programming language foundations in Agda. Sci. Comput. Program. 194, 102440 (2020). https://doi.org/10.1016/J.SCICO.2020.102440 Lindley, S., Morris, J.G.: A semantics for propositions as sessions. In: Vitek, J. (ed.) Programming Languages and Systems—24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, 11–18 April 2015. Proceedings. Lecture Notes in Computer Science, vol. 9032, pp. 560–584. Springer (2015). https://doi.org/10.1007/978-3-662-46669-8_23 McBride, C.: Everybody’s got to be somewhere. In: Atkey, R., Lindley, S. (eds.) Proceedings of the 7th Workshop on Mathematically Structured Functional Programming, MSFP@FSCD 2018, Oxford, UK, 8th July 2018. EPTCS, vol. 275, pp. 53–69 (2018). https://doi.org/10.4204/EPTCS.275.6 O’Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bull. Symb. Log. 5(2), 215–244 (1999). https://doi.org/10.2307/421090 Padovani, L., Raffaelli, C.: Agda Formalisation of the Linear Calculus of Continuations (2025). https://github.com/boystrange/LinearityChallenge. Accessed 29 Dec 2025 Padovani, L.: A simple library implementation of binary sessions. J. Funct. Program. 27, 4 (2017). https://doi.org/10.1017/S0956796816000289 Power, J., Webster, C.: Working with linear logic in COQ. In: Work-in-Progress Paper at the 12th International Conference on Theorem Proving in Higher-Order Logics, 1999 (1999) Rouvoet, A., Poulsen, C.B., Krebbers, R., Visser, E.: Intrinsically-typed definitional interpreters for linear, session-typed languages. In: Blanchette, J., Hritcu, C. (eds.) Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, 20–21 January 2020, pp. 284–298. ACM (2020). https://doi.org/10.1145/3372885.3373818 Sano, C., Kavanagh, R., Pientka, B.: Mechanizing session-types using a structural view: enforcing linearity without linearity. Proc. ACM Program. Lang. 7(OOPSLA2), 374–399 (2023). https://doi.org/10.1145/3622810 Thiemann, P.: Intrinsically-typed mechanized semantics for session types. In: Komendantskaya, E. (ed.) Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, PPDP 2019, Porto, Portugal, 7–9 October 2019, pp. 19–11915. ACM (2019). https://doi.org/10.1145/3354166.3354184 Tirore, D.L., Bengtson, J., Carbone, M.: Multiparty asynchronous session types: a mechanised proof of subject reduction. In: Aldrich, J., Silva, A. (eds.) 39th European Conference on Object-Oriented Programming, ECOOP 2025, Bergen, Norway, 30 June–2 July 2025. LIPIcs, vol. 333, pp. 31–13130. Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2025). https://doi.org/10.4230/LIPICS.ECOOP.2025.31 Vasconcelos, V.T.: Fundamentals of session types. Inf. Comput. 217, 52–70 (2012). https://doi.org/10.1016/J.IC.2012.05.002 Wadler, P.: Propositions as sessions. J. Funct. Program. 24(2–3), 384–418 (2014). https://doi.org/10.1017/S095679681400001X Xavier, B., Olarte, C., Reis, G., Nigam, V.: Mechanizing focused linear logic in COQ. In: Alves, S., Wasserman, R. (eds.) 12th Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2017, Brasília, Brazil, 23–24 September 2017. Electronic Notes in Theoretical Computer Science, pp. 219–236. Elsevier (2017). https://doi.org/10.1016/J.ENTCS.2018.10.014 Zackon, D., Sano, C., Momigliano, A., Pientka, B.: Split decisions: explicit contexts for substructural languages. In: Stark, K., Timany, A., Blazy, S., Tabareau, N. (eds.) Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2025, Denver, CO, USA, 20–21 January 2025, pp. 257–271. ACM (2025). https://doi.org/10.1145/3703595.3705888 Zalakain, U., Dardha, O.: \(\pi \) with leftovers: a mechanisation in Agda. In: Peters, K., Willemse, T.A.C. (eds.) Formal Techniques for Distributed Objects, Components, and Systems—41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, 14–18 June 2021, Proceedings. Lecture Notes in Computer Science, vol. 12719, pp. 157–174. Springer (2021). https://doi.org/10.1007/978-3-030-78089-0_9 Acknowledgements The authors are grateful to the anonymous reviewers for the detailed and constructive feedback they have provided on an early version of the paper. Funding Open access funding provided by Alma Mater Studiorum - Università di Bologna within the CRUI-CARE Agreement. Author information Authors and Affiliations Contributions CR developed the initial Agda formalisation and reviewed the existing related work. LP refined and extended the formalisation and wrote the main manuscript text. All authors reviewed the manuscript. Corresponding author Additional information Publisher's Note Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations. Rights and permissions Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/. About this article Cite this article Padovani, L., Raffaelli, C. A Continuation-Based Solution of the Linearity Challenge. J Autom Reasoning 70, 19 (2026). https://doi.org/10.1007/s10817-026-09765-w Received: Accepted: Published: Version of record: DOI: https://doi.org/10.1007/s10817-026-09765-w