Contrasting Deadlock-Free Session Processes
Abstract
Deadlock freedom is a crucial property for message-passing programs. Over the years, several different type systems for concurrent processes that ensure deadlock freedom have been proposed; this diversity raises the question of how they compare. We address this question, considering two type systems not covered in prior work: Kokke et al.’s , a type system based on a linear logic with hypersequents, and Padovani’s priority-based type system for asynchronous processes, dubbed . Their distinctive features make formal comparisons relevant and challenging. Our findings are two-fold: (1) the hypersequent setting does not drastically change the class of deadlock-free processes induced by linear logic, and (2) we relate the classes of deadlock-free processes induced by and . We prove that our results hold under both synchronous and asynchronous communication. Our results provide new insights into the essential mechanisms involved in statically avoiding deadlocks in concurrency.
Keywords and phrases:
session types, process calculi, deadlock freedomFunding:
Juan C. Jaramillo: Ministry of Science of Colombia (Minciencias).Copyright and License:
![[Uncaptioned image]](x1.png)
2012 ACM Subject Classification:
Theory of computation Type structures ; Theory of computation Program analysis ; Theory of computation Process calculiAcknowledgements:
We are grateful to Channa Dias Perera for initial discussions on the topics of this paper. We also thank Andreia Mordido and the anonymous reviewers for their helpful suggestions.Editors:
Jonathan Aldrich and Alexandra SilvaSeries and Publisher:

1 Introduction
The deadlock freedom property (DF, in the following) is a crucial guarantee for message-passing programs. Informally, DF ensures that processes “never get stuck” – an essential requirement in concurrent and distributed software systems, where even a single component that becomes permanently blocked while waiting for a message can compromise reliability. As illustration, consider a toy concurrent program in the language of Gay and Vasconcelos [14]:
We have two concurrent threads, each running an expression with two actions in sequence. This program is evaluated under a context that binds together and and declares them as endpoints of the same linear channel (same for and ); we omit it for readability. Given a linear channel , “” sends value along and returns the continuation of , whereas “” returns a pair with the continuation of and a received value. The threads are thus engaged in separate but intertwined protocols (one along , the other along ). Each thread should receive on a channel and then send a value on the other. However, the output matching the input in one thread is blocked in the other – the program is stuck. The key challenge in enforcing DF is thus performing the non-local analysis needed to avoid circular dependencies between threads, which are often less apparent than in this program.
An expressive model for concurrent processes, the -calculus offers a convenient basis for developing analysis techniques for message-passing programs in different paradigms [32]. Several type systems that enforce (forms of) DF have been proposed over the years (see, e.g., [21, 11, 5, 27, 7, 34, 1]). They avoid circular dependencies in processes using different insights, which raises the question of how they compare. In this paper, we rigorously compare some representative type systems for DF to better understand their underlying mechanisms.
A key motivation for studying type systems for concurrent processes is their suitability for developing advanced analysis techniques at an appropriate level of abstraction – these typed frameworks have been directly incorporated into languages such as Scala [33], OCaml [28, 17], and Rust [24]. Also, concurrent processes offer an adequate representation level for verifying liveness properties in real Go programs [25, 26]. Moreover, type systems for the -calculus are the basis for static analyzers (such as Kobayashi’s TyPiCal [20]) and can be ported to enforce DF for higher-order concurrent programs [29]. Type systems based on the Curry-Howard correspondence between session types and linear logic (“propositions-as-sessions” [3, 37]) enforce DF; they entail topological invariants on processes, key to ensure deadlock and memory leak freedom in concurrent programs [18]. Further understanding the essential mechanisms that enforce DF in logic-based session types is a central topic in our work.
Prior work by Dardha and Pérez [9] contrasts type systems for DF by relating the classes of processes they induce. They compare a priority-based type system by Kobayashi [21] and a type system derived from “propositions-as-sessions”. Writing and to denote the respective classes of processes, a result in [9] is that : there exist deadlock-free processes that cannot be typed by logic-based type systems. The class includes, for instance, process networks organized in circular topologies (e.g., the dinning philosophers). It also includes process below, in which two processes interact along independent protocols (sessions):
Above, “” declares a new session with linear endpoints and , and “” (resp. “”) denotes an input (resp. output of value ) along with continuation . is the deadlock-free variant of the program given above, now neatly specified as a process. In , processes can share at most one session in parallel, whereas processes in share two: the session “” for exchanging “” and the session “” for exchanging “”. In [9], both compared classes rely on a reduction semantics; accordingly, DF concerns the absence of stable states with pending reduction steps on linear names/channels.
Here we extend the work in [9] by considering type systems not studied there: (i) Kokke et al.’s [23] and (ii) Padovani’s priority-based type system [27], here dubbed . Their distinctive features make formal comparisons relevant and challenging, as we discuss next.
Derived from “propositions-as-sessions”, is based on a presentation of classical linear logic (CLL) with hypersequents. has been studied in several works, which have deepened into its theory and applications [22, 12, 31]. In , the semantics of processes is given by a Labeled Transition System (LTS), rather than by a reduction semantics. This unlocks the use of well-established analysis techniques, notably observational equivalences, to reason about typed processes. The (typed) LTS for includes the usual rules for observing actions and synchronizations, here dubbed regular transitions, but also rules that allow for delayed actions (i.e., observable actions due to prefixes not at top-level) and self-synchronizations (i.e., internal actions that do not require the interaction of two parallel processes). Remarkably, the bisimilarity induced by the LTS coincides, in a fully-abstract way, with a denotational equivalence over processes – this gives a strong justification for the design of the LTS. Typing ensures progress: well-typed processes not equivalent to always have a transition step.
An intriguing observation is that there are processes that are stuck in a reduction-based setting but have synchronizations under ’s LTS. We discuss two interesting examples, using “” and “” to denote empty inputs and outputs, respectively:
-
Process is self-synchronizing: it does not have any reductions, whereas , as in synchronizations do not need a parallel context to be enabled.
-
Process is arguably the paradigmatic example of a deadlock, with two independent sessions unable to reduce. In , thanks to delayed actions, we have both and .
This observation shows that comparisons such as [9] should accommodate other semantics for processes, beyond reductions, which entail other definitions of DF and induce new deadlock-free processes (such as and ). This begs a first question:
- (Q1)
-
What is the status of delayed actions and self-synchronizations, as typable in , with respect to DF? Do they induce a distinct class of deadlock-free processes?
Considering Padovani’s means addressing the case of processes with asynchronous communication, widely used in real programs. In the -calculus, asynchronous communication is obtained by defining outputs as non-blocking actions; only inputs can block the execution of a process [2, 16]. Asynchrony and DF are then closely related: because an asynchronous setting involves the least amount of blocking operations, it offers the most elementary scenario for investigating DF [35]. Now, the comparisons in [9] are limited to synchronous processes; we then observe that they should be extended to address asynchronous communication, too. Let us write and to denote the class of processes induced by and , respectively, and to denote the class of processes induced by (a fragment of without hypersequents and with a restricted form of parallel composition). We consider the second question:
- (Q2)
-
What is the status of and with respect to asynchronous processes in ?
Interestingly, our two questions are intertwined: and are related due to asynchrony. Our insight is that delayed actions in already implement an asynchronous semantics. To see this, consider the process , which is not stuck: the output on is not really blocking, as delayed actions allow to anticipate the output (and synchronization) on . In other words, is morally the same as . We thus conclude that the (typed) operational semantics for admits many synchronous-looking processes (such as ) that actually behave in an asynchronous way; this naturally invites the question of how relates to .
Contributions and Outline.
This paper offers conceptual and technical contributions. From a conceptual view, we reflect upon the significance of formally comparing different type systems for concurrency, while uniformly presenting various notions in the literature. On the technical side, we address (Q1) and (Q2), thus extending and complementing [9]. A key discovery is identifying commuting conversions and disentanglement as key notions for characterizing deadlock-free processes in – as we will see, these notions define sound process optimizations that respect causality and increase parallelism. As our results hold also in an asynchronous setting, not treated in prior work, our findings are most related to abstractions and mechanisms used in practical concurrent programming. More in detail:
- § 2
-
We introduce , a session -calculus that we use as baseline for comparisons, as well as and , the type systems resulting from the Curry-Howard correspondence with CLL and CLL with hypersequents, respectively.
- § 3
-
We define and : the classes of deadlock-free processes induced by and , respectively. We identify two relevant sub-classes of :
- :
-
Processes that use the LTS.
- :
-
Processes that only use egular transitions (no delayed actions/self-synchronizations).
In our main result (Corollary 53), we prove that for every process , there exists an observationally equivalent process . Enabled by process optimizations induced via commuting conversions and disentanglement, this result shows that delayed actions and self-synchronizations are inessential when it comes to DF, addressing (Q1).
- § 4
-
To address (Q2), we define : the class of deadlock free processes induced by , and its sub-class (“micro ”), which is inspired by . We prove that (Corollary 74), thus casting Dardha and Pérez’s key finding into the asynchronous setting. Our main results are: Theorem 76, which precisely relates the classes , , , and ; and Corollary 77, which strengthens Corollary 53 by considering DF in . Moreover, we introduce , an asynchronous variant of , and its corresponding classes of processes. We show how to transfer Theorems 76 and 77 from to (Corollary 88).
Figure 1 offers a graphical description of the classes of processes and some of our main results (Corollaries 53, 74, and 76). For simplicity, the figure does not depict several encodings needed to bridge syntactic differences between the various classes of processes / type systems under consideration; Figure 12 (Page 12) presents a detailed version. In § 5 we collect some closing remarks. The extended version of the paper [19] contains omitted proofs.
2 Session Processes and Their Type Systems
We present , our reference language of session processes. As observed by Dardha and Pérez [9], this is a convenient framework for formal comparisons, because typing in ensures communication safety but not DF. We also present and , the two typed languages based on “propositions-as-sessions”, and recall useful associated results.
2.1 Session Processes ()
is a core session-typed -calculus, based on the language defined by Vasconcelos [36]. We assume a base set of variables, ranged over by , which denote channels (or names): they can be seen as endpoints on which interaction takes place. Processes interact to exchange values ; for simplicity, values correspond to variables, i.e., . We write to denote a finite sequence of variables. The syntax of processes is as follows:
Process denotes inaction. Process sends along and continues as . Process receives along and continues as , i.e., the process resulting from the capture-avoiding substitution of by in . Process denotes the parallel execution of and . Process declares and as co-variables, restricting their scope to . That is, restriction declares co-variables as dual ends of a channel. Finally, and denote empty output and input (close and wait), which represent the closing of session .
As usual, binds in and binds in . The sets of free and bound variables of , denoted and , are defined accordingly. The semantics of processes is given using a reduction relation, defined next.
Definition 1 (: Reduction).
We now define session types, which express protocols associated to channels:
Definition 2 (: Session Types and Typing Environments).
The syntax of session types and typing environments is inductively defined as follows:
The type (resp. ) is assigned to a channel able to send (resp. receive) a value of type and to continue as . For convenience, we have two different types for channels with terminated protocols, denoted and . Duality on types ensures that the endpoints of a channel agree on the protocol they describe:
Definition 3 (: Duality).
The dual of , denoted , is defined as follows:
Definition 4 (: Typing Judgment and Typing Rules).
The judgment describes a well-typed process under the typing environment . The typing rules for are shown in Figure 3. We shall write if , for some .
We now state the properties of well-typed processes, whose proofs follow [36]:
Theorem 5 (: Preservation [36]).
Suppose . If then . Also, if then .
We will be interested in well-formed processes, defined using two auxiliary notions. First, we say that is prefixed at , written , if has one of the following forms: , , , or . Second, we say a process is a redex if: (1) and , or (2) and . We may now define:
Definition 6 (: Well-formedness).
A process is well-formed if for each of its structural congruent processes of the form where and , then is a redex.
Theorem 7 (Safety [36]).
Typable processes are well-formed.
As a consequence of Theorems 5 and 7 we obtain the main guarantee of : typable processes only reduce to well-formed processes.
Corollary 8 ([36]).
If and , then is well-formed.
Even though typability ensures well-formedness, which excludes error processes such as and , typability in also admits well-typed process that exhibit unwanted behaviors, in particular deadlocks. Before illustrating this fact, we give the first definition of deadlock freedom that we will encounter, which follows [9]. We write to stand for , for some .
Definition 9 (: Deadlock Freedom).
A process is deadlock free, written , if the following condition holds: whenever and one of the following holds: (1) , (2) , (3) , or (4) (with in all cases), then , for some .
Hence, is read as “ is deadlock-free in ”. Later on, we will encounter analogous notations for and ; they will be denoted and , respectively.
Example 10 (: A Typable but Deadlocked Process).
Consider the process defined as
where and . Similar to (§ 1), the structure of actions in process induces a circular dependency that prevents synchronizations: we have that and yet is well-typed with the empty environment.
2.2 and
The languages and use the same syntax. Here we consider as presented by Kokke et al. [23] (other variants have been studied in, e.g., [13]). Assuming an infinite set of names (), the set of processes () in and is defined as follows:
Most constructs are similar to those in ; differences are the forwarder process , which equates and , and process , which denotes the output of the private name along , with continuation . Also, the empty output is now denoted . In and , the name is bound in . We write to denote the capture-avoiding substitution of for in . We write to denote the free names of . We use to range over prefixes: , .
The types assigned to names correspond to formulas of classical linear logic (CLL):
The assignment says that follows the input/output interactions described by . Assignments and are read as sending and receiving an object of type along , with continuation , respectively. There is a duality in the interpretation of the following pairs: and ; and . Formally, the dual type of , denoted , is defined as
Let range over environments, unordered collections of assignments. Given an environment , its domain, written , is the set .
Definition 11 ().
Typing judgements for are of the form , with typing rules as given in Figure 4. We shall write if , for some .
Observe how typing in induces a specific shape for output processes: . This is not the case in , where processes are described by hyperenvironments, unordered collections of environments: .
Definition 12 ().
Typing judgements for are of the form , with typing rules as given in Figure 5. We shall write if , for some .
and differ in process composition, which is key to exclude the circular dependencies that lead to deadlocks: it is realized by Rule C-Cut in and Rule H-Cut in . The former requires two premises describing processes that share exactly one session; typing involves both composition and restriction and induces tree-like process topologies. The latter involves one premise only, which describes a process in which the separation between and is made explicit by “” at the level of hyperenvironments; typing involves restriction only.
Every typable in is also typable in , but the converse does not hold. We have:
Lemma 13 (Relation Between and [23]).
If then .
Example 14 (The converse of Lemma 13 does not hold).
To illustrate a process typable in but not in , consider , where:
We have . First, follows from several applications of Rules H- and H-. To type , we first obtain , crucially using Rule H-Mix2 several times to compose the four independent processes. Because , by Rules H-Mix2 and H- we have: . We proceed similarly to type the output on and complete the typing of . Finally, to compose and we apply H-Mix2 and H-Cut.
Now, cannot be typed in : there is no rule similar to Rule H-Mix2, which can compose independent processes. Hence, is not typable in .
In general, the composition of two processes that share more than one session cannot be typed in . Now consider :
Observe how modifies by keeping unchanged and dividing the two outputs in into threads that can be composed separately using Rule C-Cut. We have .
Given a , with , we are interested in partitioning the free names in according to the environments . These name partitions describe which names are used by each parallel component of ; they are defined considering all the different hyperenvironments under which is typable.
Definition 15 (: Name Partitions).
Given , we define . Given , its name partitions are .
holds whenever there is a such that and belong to different proper subsets of . Also, holds whenever and belong to the same proper subset of .
Example 16.
Consider the process : it can be typed under the hyperenvironments and . Given this, , and we have, e.g., and .
The semantics of is given in terms of a Labeled Transition System (LTS):
Definition 17 (: LTS).
The binary relation on processes is defined by the rules in Figure 6, with action labels defined as follows:
In the following, , , and denote the free, bound, and channel names of , respectively. They are defined as follows: , , , and . Also, , and . Moreover, .
The rules in Figure 6 are inspired by proof-theoretical transformations on ’s proof derivations [23]; they can be divided into two classes. The rules above the line are usual formulations for actions, structural rules, and communication. Actions can appear in parallel in a label, and compatible actions in parallel induce a -transition. The five rules below the line formalize delayed actions and self-synchronizations. Intuitively, the first four rules allow to observe an action in a delayed style; such an action must be independent from the prefix at the top-level (on ). The last rule, , implements self-synchronization for a process : the (top-level) prefix is considered in parallel with a (delayed) action emanating from .
Example 18.
To illustrate the LTS of , recall the processes and from § 1. In , they are denoted as: and . Consider the following type derivation, parametric on :
Thus, is typed as followed by an application of Rule H-Cut. Also, is typed by and followed by an application of Rules H-Mix2 and H-Cut. Because Rule only types empty outputs followed by , neither nor are typable in .
By Rules and in Figure 6, . Similarly, by Rules and syn. Finally, by Rule , .
We now recall some useful notions and results from [23].
Definition 19 (: Weak LTS and Bisimilarity [23]).
is the smallest relation such that:
(1) for all ;
(2) and if , , and , then .
A symmetric relation is a bisimulation if implies that if then for some such that . Bisimilarity is the largest relation that is a bisimulation.
Well-typed processes satisfy readiness, defined as follows:
Theorem 20 (: Readiness [23]).
Let . For every , there exist , , and such that .
In , transitions associated to sessions in different partitions can be fired in parallel:
Lemma 21 ([23]).
If , , and , then there exists s.t. (up to -renaming).
Definition 22 (: Structural Congruence).
Let be the smallest congruence relation generated by the axioms:
Because of Readiness (Theorem 20), also satisfies progress:
Corollary 23 (: Progress [23]).
If and , then for some , .
In order to relate with reduction-based semantics (in ), we define the following:
Definition 24 (: Reduction).
We write for the reflexive, transitive closure of .
Lemma 25.
Let s.t. , then exists s.t. .
Proof sketch.
We prove it in two steps: (1) We prove that if , then there exists s.t. , and . This ensures the existence of a -transition in every step. (2) We then prove that can be reached in finitely many steps. See [19] for details.
Inspired by Lemma 25 we have the following definition of deadlock freedom for .
Definition 26 (: Deadlock Freedom).
Let . We say that is deadlock free, written , iff there exists s.t. .
has a denotational semantics that interprets well-typed processes as sets of possible interactions on their free names. Given a process , its set of denotations is written . Denotational equivalence, noted , is the typed relation defined as: iff . We shall rely on denotational equivalence; its exact formulation, given in [19], is interesting but not crucial for following our results. We notice that is sound wrt and that our results are reflected by bisimilarity, as ensured by the following result:
Theorem 27 (: Full Abstraction [23]).
For well-typed processes: .
3 The Role of Delayed Actions and Self-Synchronizations in DF
We have seen that defines a flexible typing discipline that admits deadlocked and deadlock-free processes. Also, we saw the way in which and enforce DF by typing, and that the latter’s LTS allows for delayed actions and self-synchronizations. By defining two classes of processes, and , which capture typability as in and , respectively (Definition 34), we study whether delayed actions and self-synchronizations influence DF.
We proceed as follows. As we have seen, means that is deadlock free by considering all sources of behavior, including delayed actions and self-synchronizations; we shall also define to mean that is deadlock free by considering regular transitions only. Our main result is Corollary 53, which ensures: (1) delayed actions and self-synchronizations are inessential when it comes to DF, and (2) given an encoding , for a process such that , there is a that simulates , and .
3.1 From to
We start by translating processes in into processes in :
Definition 28.
Let . The encoding is a homomorphism except for the case of free output, defined as . For types, we define:
For typing environments, we define: and .
Regular Transitions do not depend on self-synchronizations or delayed actions:
Definition 29 (: Regular Transitions).
A derivation for is denoted . We define iff is derived only using rules above the horizontal line in Figure 6.
Example 30.
Recall the processes and from Example 18, which use self-synchronizations and delayed actions, respectively: we have that , and . Therefore, and .
The encoding of free output induces transitions involving the forwarder process, not present in the source process. We handle the substitutions induced by forwarders in Rule AxCut (Figure 6) as follows:
Definition 31 (: Ready-for-Substitution).
Let . We say that is ready for substitution of for , written , if there exists and s.t. , and . Otherwise, we write .
We may now define transitions for processes that are ready for a substitution.
Definition 32 (: Eager-to-Rename).
The relation on processes is defined as:
Intuitively, executes outputs and forwarders in one single step. When only relies on regular transitions we have the following operational correspondence result.
Theorem 33 (: Operational Correspondence).
Let .
-
1.
If and , then s.t. .
-
2.
If , then s.t. .
Proof sketch.
Part (1) is proven by case analysis in , and (2) is proven by induction in the derivation of . See [19] for details.
Following Dardha and Pérez [9], we now define and as the classes of processes that are also typable in and , respectively:
Definition 34 (Classes and ).
The classes and of processes are defined as:
Hence, in writing “” we are not referring to an process directly, but rather to a process (in the sense of § 2.1) that is related (up to ) to some (typable) process. This is how offers a unifying framework for comparing different type systems. As a direct consequence of Lemma 13 and Example 14 we have that .
3.2 A Refined Account of , Based on Deadlock Freedom
As explained in the previous section, enjoys liveness properties corresponding to the LTS. If we focus only on -transitions (cf. Definition 24) we obtain the following results.
We extend Definition 29 (regular transitions) to sequences of transitions, as follows:
Definition 35 (: Regular Sequence of Transitions).
Assume in and transitions . We say that a transition sequence transitions regularly iff for all . We write .
We are interested in processes whose transitions are regular, thus we refine deadlock freedom in (Definition 26) as follows:
Definition 36 (: Deadlock Freedom based on Regular Transitions).
Let . We say that is deadlock free without delayed actions and self-synchronizations, written , iff , , and .
In turn, Definitions 26 and 36 allow us to refine the definition of (Definition 34):
Definition 37 (: Sub-classes of ).
We define the following classes of DF processes:
By Definitions 34 and 37 we have .
Example 38.
Consider the processes:
We have and . Although , the process has a -transition due to a delayed action, and therefore .
Theorem 39.
If , then .
Proof.
It follows from Theorem 33 and Definitions 37 and 9.
From to via process optimizations.
We now embark to show how to transform processes in (where self-synchronizations and delayed actions are used) into processes in (where they are not). Intuitively, we would like to transform, e.g.,
The transformation from to is formalized by Theorem 47. To achieve it, we leverage two existing ingredients. The first ingredient is the notion of commuting conversions: sound transformations on processes that involve actions from independent sessions (cf. [10, 30]).
Definition 40 (: Commuting Conversions).
We define as the smallest congruence on processes induced by the equalities in Figure 7.
The transformations induced by have a proof-theoretical origin, and so they are type-preserving, which ensures that they do not alter the causality relations on processes. We can show that that is sound wrt , i.e., if then .
Example 41.
Recall processes , , and from Example 14. We illustrate the optimizations on processes induced by commuting conversions by combining and the process , as follows:
Note that a -transition along the sessions or in would depend on a delayed action. Now, we can use a commuting conversion to swap the order of the inputs, effectively anticipating the input on : ; therefore, . Clearly, there is a transition sequence s.t. .
The second ingredient is disentanglement, which also induces optimizations on processes:
Definition 42 (: Disentanglement [22]).
Disentanglement is described by the smallest relation on (typed) processes closed under the rules in Figure 8. We write for the reflexive and transitive closure of .
Each of the process transformations in Figure 8 is justified by an operation on derivations; this way, e.g., for the second rule we have:
This way, disentanglement proceeds by the repeated application of the rules from Figure 8 to the derivation of , which aims at moving downwards the instances of Rule H-Mix2 (cf. Figure 5). If H-Mix2 gets stuck in either H-Cut or , then it becomes an instance of C-Cut or , respectively (cf. Figure 4).
Disentanglement increases the parallelism in processes. This way, e.g., for and (Example 14) we have: . Also, note that Rule types , induces a discrepancy: at the process level, the rule places the empty output in sequential composition with , whereas at the level of typing is placed in its own partition, enforcing independence from all names in . Disentanglement solves this discrepancy. Consider, e.g., process : we have .
Lemma 43 (Disentanglement [23]).
If there exists a derivation of , then there exist derivations of in , and
where we use the double line to indicate multiple uses of the same rule.
The following result ensures that process observations are invariant under disentanglement. Moreover, since instances of H-Cut are turned into instances of C-Cut, disentangled processes do not feature occurrences of restriction between sessions in sequential composition.
Lemma 44.
Suppose . If then .
Proof.
We prove that if then by induction on the length of . For the base case () we proceed by a case analysis in the last rule applied in the type derivation of . The fact that follows from Theorem 27.
Given a process , the rules for disentanglement can be applied in any order; we therefore define a set of disentangled processes:
Definition 45 (: Disentangled Processes).
Given , the set is defined as follows:
From Lemma 44 we have that all disentangled processes are observationally equivalent:
Lemma 46.
Let . If , then .
Proof.
From Lemma 44, for all . By Definition 19, is transitive. Hence, for all , . We use disentanglement to prove that if then there is a s.t. , with .
The following main result establishes that the notions of (Definition 26) and (Definition 36) are equivalent, up to commuting conversions and disentanglement.
Theorem 47.
For all processes s.t. , then there exist s.t.: (1) , (2) , (3) , (4) .
Proof sketch.
Parts (1)-(3) follow from Definitions 45, 40, and 44. For part (4) we show that self-synchronizations and delayed actions are eliminated by means of disentanglement and commuting conversions, respectively. See [19] for details.
Theorem 47 concerns processes. To lift this result to , we need some results.
Lemma 48.
Let . There exists s.t.: (1) . (2) .
Proof.
The items follow by induction on the length of and , respectively. For (1) in the base cases we proceed by a case analysis in the last rule applied in the type derivation of ; it shows the structure of and by Definition 28 we obtain the structure of . The proof finishes by applying a single step of to the type derivation of and replicating it to the derivation of . The proof of (2) proceeds similarly.
Lemma 48 ensures that the following definition is sound:
Definition 49 (Lifting Commuting Conversions and Disentanglement to ).
Let . We write and , whenever and hold, respectively.
Having disentanglement in , we aim to prove that the resulting disentangled process simulates the original process. To define simulation in , we need the following notion:
Definition 50 (: Labelled Reduction Semantics).
Let , then whenever:
(1) , or (2) .
Definition 51 (: Simulation).
A binary relation in is a (typed) simulation if whenever then , and implies for some s.t. . We write whenever for a (typed) simulation .
In the LTS semantics of , the processes and from Theorem 47 are bisimilar; however, in a reduction semantics, any transitions of that use delayed actions or self-synchronization would be considered as deadlocks, and then would only simulate . Formally:
Theorem 52.
The relation is a simulation.
Proof sketch.
By induction in the structure of , with a case analysis in . See [19] for details.
Finally, Corollary 53, given below, brings Theorem 47 to : it shows that even though in both and are equivalent, in those notions are related via a simulation.
Corollary 53.
Given , then there exist and s.t.: (1) , (2) , (3) , (4) .
Proof.
It follows by Lemmata 48, 47, and 52.
Example 54 (Corollary 53, At Work).
Consider the process and its encoding into :
Note that but has two -transitions:
(1) | ||||
(2) |
where the transition in (1) is due to a delayed action on and a self-synchronization along the session , and the transition in (2) is due to a delayed -transition along the session . Hence, . Via disentanglement we obtain:
In , neither a delayed action nor a self-synchronization are needed, thus . We could also give priority to the -transition along ; however, because the input on is not at the top-level, a synchronization on still requires a delayed action. This shows the need for commuting conversions. Indeed, by using we obtain:
We have that . Moreover, there is a process in s.t. :
Notice that follows trivially since .
4 The Case of Asynchronous Processes
Up to here we have addressed (Q1) by considering the relation between and in . We now turn our attention to (Q2) and consider the interplay of DF and asynchronous processes as typable by Padovani’s type system for asynchronous processes, here dubbed [27].
We proceed as follows. In § 4.1 we recall Padovani’s type system and introduce , the class of processes induced by , and its sub-class , derived from the type system . In § 4.2, we show that (Corollary 74). In § 4.3, we establish a key result: the precise relations between , , , and (Theorem 76). Also, we revisit Corollary 53 from the standpoint of : we prove that the process (obtained via commuting conversions and disentanglement) is also in (Corollary 77). In § 4.4 we present , an asynchronous version of , and show how to extend our results for to (Corollary 88).
Table 1 summarizes all technical ingredients, including those introduced in this section.
4.1 The Type System
We summarize the linear fragment of the type system by Padovani [27], which streamlines Kobayashi’s type system for deadlock freedom [21]. We assume sets of channels and variables ; then, names are either channels or variables. We find it convenient to use processes with polyadic communication:
Two salient features are the output , which does not have a continuation, and “”, the standard restriction construct of the -calculus. Notions of free and bound names are as usual: in the process , are bound in ; in , is bound in . We write and for the free and bound names of , respectively.
The reduction semantics is closed under a structural congruence, denoted , which is standardly defined by the following axioms: (i) , (ii) , (iii) , (iv) (if ), and (v) .
Reduction is then defined as
Example 55.
Differently from , channels in Padovani’s framework are used exactly once. Structured communications can of course be still expressed, using continuations. Consider the process with
sends the two endpoints of a channel: the first is sent along (together with a continuation channel ), and the other is sent along . Channel occurs in both outputs, but these occurrences actually denote different endpoints; this difference will be justified by typing (cf. Example 59). receives these endpoints to implement a local exchange of name along .
Padovani’s type system ensures the absence of pending communications in a process with respect to a channel. To formalize this notion, we rely on reduction contexts, defined as . We may now define the following auxiliary predicates:
Intuitively, predicate holds if is free in and there is a subprocess of that can perform a linear input on . Predicate holds if is free in and a subprocess of is waiting to send a value . Predicate denotes a pending input/output on for which a synchronization on is immediately available. This way, to formalize a pending input/output for which a synchronization on is not immediately possible, we define:
Thus, ensuring no pending communications in means ensuring for every .
Example 56 (Predicates at work).
Consider the process , which has a circular dependency. We have: (1) and . (2) and . (3) and . (4) and .
Type System.
To ensure absence of pending communications, relies on priorities. Let denote subsets of (polarities). Types for channels are defined as follows:
where is the priority of a channel, which indicates urgency for its use: the lower the number, the higher the urgency. We write # for . This way, # and are even polarities.
Example 57 (Priorities).
To illustrate types and priorities, recall again the process . As we have seen, we have and .
Let us assume that are all typed with some type . By inspecting the left thread of , we infer that and must be typed as and , respectively, for some . Then, by inspecting the right thread, we infer that and must then be typed with and , respectively. This way, their types in the composed process are (for ) and (for ). Looking again at the left thread, as the input along is blocking the output along , we must have ; in the right thread we have the exact opposite situation, thus . These unsolvable inequalities reveal the circular dependency between and , which will make not typable in the type system .
We now summarize how typing excludes pending communications. Type environments are finite maps from channels to types. We write for the domain of . We write for the union of and when . We write to denote a partial composition operator on types defined as: if , and undefined otherwise. For type environments we have: if , and . Let , where for every . The functions , from types to , and from types to types are defined as follows:
Intuitively, the function allows us to shift priorities. We say that a type is unlimited, written , iff . We write iff all the types in the range of are unlimited. We are now ready to give the typing rules, considering only processes with biadic communication, for simplicity. The rules for monadic communication are as expected.
Definition 58 ().
The typing rules for processes use judgements of the form and and are presented in Figure 9. We shall write if , for some .
Rule T-In is used to type inputs , where has type . The condition ensures that has been assigned the highest urgency; accordingly, the types of and are shifted by . Rule T-Out, used to type outputs on channels of type , follows a similar principle: the types of and are shifted by , since they must have lower urgency than . Rule T-New is used for restricting new channels with full (#) or empty () polarity.
Example 59.
Recall processes and from Example 55. Consider types and . Note that . Process is typed as follows:
Similarly we can check that . Note that is typed with opposite polarities in and ; thus by applying Rules T-Par and T-New we obtain .
We may now characterize deadlock freedom. Let us write to denote the reflexive, transitive closure of . Also, write if there is no such that . We have:
Definition 60 (: Deadlock Freedom [27]).
We say that is deadlock free, written , if for every such that we have for every .
We have that processes typed in the empty environment are deadlock free:
Theorem 61 (: Deadlock Freedom [27]).
If , then .
4.2 Relating and
We now consider (“micro ”), which is a fragment of that is similar to . We also define the encoding , and and the classes of processes that are captured by and , respectively. These are all ingredients for our results in § 4.3.
Definition 62 ().
The typing rules for processes are presented in Figure 10. A judgement denotes that is well typed in . We shall write if , for some .
results from by replacing Rules T-Par and T-New in Figure 9 with Rule M-New-Par, which combines restriction and parallel just as Rule C-Cut in Figure 4.
Lemma 63.
If then .
Proof sketch.
By induction on the type derivation, with a case analysis in the last rule applied. See [19] for details.
Corollary 64.
If , then .
Proof.
It follows by Lemmata 63 and 61. We now define an encoding from to , following a continuation-passing style (cf. [8]). Let be a function from names to names. We use the following conventions: stands for , and stands for the function s.t. and if .
Definition 65.
The (partial) encoding is parameterized by a function, ranging over , from names to names, and is defined for processes as follows:
and as a homomorphism for and . The encoding of session types is as follows:
Typing environments are encoded inductively as and . The values of and are calculated when checking in the typablity of .
Intuitively, the encoding of processes in Definition 65 collapses the two endpoints of a session into a single name in . The encoding of mimics both the sequential structure of a session and synchronous communication. sends the (renamed) value and a new channel along which an input blocks the continuation , and receives the channel along which the the continuation of the session will be sent. Dually, receives the intended value and the channel , which sends the channel , along which the continuation of the session will be received. Finally, the encoding is partial because is only defined when : this allows us to characterize the session processes captured in , where the empty output has no continuation (see Definition 11).
Example 66.
Consider the process in . We show and illustrate its reductions. Let us assume is well-typed. Because of linearity of and , they only appear in the left and right subprocess, respectively. Let and ,, then we have:
Our main result concerns the classes of processes associated to and , which we define by mirroring the definition of and (Definition 34):
Definition 67 ( and ).
The classes of processes and are defined as follows:
The following result establishes an operational correspondence between a process and its encoding, what will allows us to capture deadlock free session processes via the encoding.
Theorem 68 (Operational Correspondence for ).
Let . We have:
-
1.
-
(a)
If , then such that and .
-
(b)
If , then such that and .
-
(a)
-
2.
If , then either:
-
(a)
such that and , or
-
(b)
, and such that , and .
-
(a)
Proof.
By assumption, and so we have that , for some , and is defined. Moreover, by Corollary 8 is well-formed. We consider each item separately. Item 1(b) follows by Definition 65 and the rest of the analysis proceeds as in Example 66; Item 1(a) is similar. Item (2): If , then . By typability of and Definition 65 one of the two possibilities apply:
-
i
, , and ,
-
ii
and
In case (i) and , which verifies case (2a). In case (ii) we proceed as in Example 66, which verifies case (2b).
As a consequence of Theorem 68 we have the following result, which shows the relation between deadlock-free processes in .
Corollary 69.
Let . iff .
Proof.
For each direction we prove its contrapositive. We discuss only the right-to-left direction; the analysis for the left-to-right direction is similar. By Definition 60, there exist and s.t. and . If holds because then . By Theorems 68 and 65 there exists s.t. and . Note that , since otherwise by Theorem 68(1), for some process , contradicting our assumption, thus . The case when holds because proceeds similarly.
Corollary 69 allows us to detect DF session processes via the encoding.
4.3 Comparing and
From § 3 we infer that a process , typed as , can be decomposed into processes , , . Moreover, by Lemma 48 (disentanglement in ) we infer that processes have a pre-image in , therefore .
As an important preliminary step, we first prove that (Corollary 74). We split the proof in two separate inclusions. The following lemma is useful to prove that .
Lemma 70.
Let and be an environment and a process in , resp. The following hold:
-
1.
If , then .
-
2.
If , then .
-
3.
Let . If and , then , with fresh wrt .
-
4.
Let be typing environments in , then , for some renaming function .
-
5.
Let be a session type. Then , for some , , a type in , and even.
Proof.
(1) Proven in [27]. (2) Follows from Lemma 63 and item 1. (3) Follows by induction on the type derivation. (Figure 10). (4) Follows immediately by linearity of names in , for . (5) Follows by induction on the structure of .
Theorem 71.
.
Proof sketch.
By induction on the type derivation with a case analysis in the last rule applied. See [19] for details.
To prove the other direction we need the following result.
Lemma 72.
Let and be session types. We have: (1) is defined iff . (2) .
Proof.
Item (1) follows by Definition 65 and def. of . Item (2) follows immediately by induction in the structure of and Definition 28.
Theorem 73.
.
Proof sketch.
By induction on the type derivation with a case analysis in the last rule applied. See [19] for details.
Corollary 74.
.
Proof.
It follows by Theorems 71 and 73.
Main Results.
We may now return to considering . Note that : to see this, consider, e.g., the self-synchronizing process from Example 18. Using Corollary 74 and disentanglement (Definition 42) we show that given a process , we can find a deadlock-free process . Formally, we have:
Theorem 75.
Given , s.t. , , and .
Proof.
By Corollary 53, , and by Lemma 48 , there exists s.t. . From Corollaries 74 and 63 we infer , . Moreover, by repeatedly applying Rule T-Par we have that . Finally, follows from Theorems 39 and 69.
The following result relates , its subclasses and , and .
Theorem 76.
The following hold: (1) . (2) . (3) .
Proof sketch.
We give witnesses for each statement; see [19] for details.
Finally, from Theorem 75 we have the following result, which complements Corollary 53: given , there exists a bisimilar process via disentanglement. Note that this result applies in particular to processes in .
Corollary 77.
Given , there exists s.t. (1) , (2) , and (2) .
4.4 Asynchronous Session Processes
Up to here, we have considered asynchronous communication somewhat indirectly: we have examined the type system for asynchronous processes , defined its associated classes and , and related them to and . To treat asynchronous communication directly, here we consider , an asynchronous variant of , and discuss how to transfer our results from §§ 3 and 4.3 from to by leveraging an encoding .
: Asynchronous .
We define as a variant of with asynchronous communication. Considerations about variables, endpoints, and values are as for (cf. § 2.1). The syntax of processes is largely as before; only constructs for output and input are modified:
Process sends names and along : the former is a message and the latter is a continuation. Because it has no continuation, this process may be seen as an “output particle” that carries a message. Accordingly, process receives two values and along and continues as , i.e., the process resulting from the capture-avoiding substitution of by , and by in . The construct for empty output is also modified. In both and are bound in .
Definition 78 ().
The typing rules for processes are presented in Figure 11. A judgement denotes that is well typed in . We shall write if , for some .
Most typing rules are self-explanatory. Rule A-Eoutput types an empty output without continuation. Rule A-Out types the output particle where . Since the output has no continuation, the session name typed as serves a a continuation name for . Dually, Rule A-In types as provided that and are typed as and in , respectively, thus, serves as a continuation for in .
The reduction semantics for is defined as follows:
A-Com | ||||
A-EmptyCom |
Structural rules and the congruence are defined as in Figure 2. A labeled reduction semantics for follows easily from Definition 50.
Example 79.
Consider the process from Example 10, which is typable and deadlocked in . The following process can be seen as the analogue of but in the asynchronous setting of . We define as , where
Note how and serve as a continuation for and , respectively. There exist processes such that .
We define DF for by adapting Definition 9:
Definition 80 (: Deadlock Freedom).
A process is deadlock free, written , if the following holds: whenever and one of the following holds: (1) , (2) , (3) , or (4) (with in all cases) then there exists such that .
Example 81 (Comparing DF in and ).
As just illustrated by means of processes (from Example 10) and , moving to an asynchronous setting may solve certain deadlocks: we have and .
On the other hand, moving to an asynchronous setting alone does not resolve the problem. Consider the process . Clearly, is typable in . Also, let be the variant of with as continuation for outputs, i.e., . We have that is typable in and that and .
Our goal is to transfer our technical results for to the asynchronous setting of . To this end, we define the following encoding:
Definition 82.
We define the encoding from to as follows:
and as an homomorphism for , , and .
Example 83 (, At Work).
Consider again the process . We have seen that . We now check that does not add deadlocks by verifying that :
One can show that there exist such that .
By a similar analysis to the one for Theorem 68, we have the following result:
Theorem 84 (: Operational Correspondence).
Let . The following holds:
-
1.
if , then s.t. and .
-
2.
If , then s.t. and .
-
3.
If , then either: (i) there exists s.t. , and , or (ii) and .
Using Theorems 84, 9, and 80 we formalize our claim from Example 83: does not add deadlocks.
Theorem 85 (Correspondence DF).
For all , iff .
Proof sketch.
For each direction we prove its contrapositive and proceed by contradiction. See [19] for details.
Using the encoding , and inspired by Theorems 84 and 85, we can define the following classes of asynchronous processes by relying on their synchronous counterparts:
Definition 86.
The classes of asynchronous processes are defined as follows:
Each asynchronous class is contained (up to ) in its corresponding synchronous class:
Lemma 87.
Let . The following hold: (1) If , then . (2) If , then . (3) If , then . (4) If , then . (5) If , then . (6) If , then .
Proof.
It follows straightforwardly from Definition 86. Thus, we can transfer our main results (Corollaries 53, 77, and 74) to via . For instance, Corollary 53 is transferred to as follows, using Lemma 87, and Theorem 84:
Corollary 88.
Given , there exist and s.t.: (1) , (2) , (3) , (4) .
5 Closing Remarks
Enforcing DF is a relevant issue for message-passing programs, and type systems for concurrent processes offer a convenient setting to develop analysis techniques that detect insidious circular dependencies in programs. Because there exist different type systems that enforce DF, it is natural to wonder how they compare.
We have studied this question in the general and expressive setting of the -calculus. Our approach aims at establishing the key strengths and limitations of three representative type systems: , the reference language for session-typed processes; , the session-typed language based on “propositions-as-sessions” and hypersequents; and , the priority-based type system for asynchronous processes. Figure 12 gives an overview of our main technical results, refining Figure 1. We briefly discuss their broader significance. Our work can be seen as covering three dimensions of comparison: type systems (, , ), process semantics (reduction semantics and LTS), and several definitions of DF (cf. Definitions 9, 26, 36, 60, and 80). Clearly, each type system connects these dimensions in its own way via meta-theoretical results (e.g., type preservation). From this perspective, considering a type system such as , which comes with an LTS for typed processes with very distinctive features (delayed actions and self-synchronizations), brings significant value to our results. In contrast, the work of Dardha and Pérez [9] (the most closely related work) considers different type systems for synchronous processes but only under a reduction semantics, which influences the definition(s) of DF to be considered.
Our key discovery is identifying the role that commuting conversions and disentanglement have in the class of deadlock-free processes induced by (Corollary 53). Although studying the practical ramifications of our results goes beyond the scope of this paper, two observations are relevant. First, our results pave the way for developing extensions of the static analyzer TyPiCal [20] that support the mechanized analysis of (session) processes with asynchronous communication. Second, commuting conversions are already important in practical developments, such as execution strategies in abstract machines for session-typed programs [4] and definitions of session subtyping [6, 15] that enable flexible programming interfaces. An in-depth exploration of these latent connections between our results and tools for the analysis of message-passing programs is left for future work.
It is worth stressing that ’s LTS enjoys strong logical and denotational justifications; by identifying disentanglement and commuting conversions as key notions for DF, we provide new insights into and its LTS. This way, our work sheds new light into the foundations of , its positioning within the line of work on “propositions-as-sessions”, and its expressive power. For instance, it is surprising that processes that share more than one session are typable in , in the sense of Example 14. While Kokke et al. [23, 22] have studied disentanglement as a tool to relate and , here we uncover its connection with DF. Also, their work on ( with a reduction semantics but without delayed actions and self-synchronizations) is complementary to our findings. In this sense, our work also offers good motivations for the use of LTSs with regular transitions as the semantics for logic-based session processes (which usually rely on reduction semantics).
It is remarkable that and are not just two type systems relevant for a formal comparison, but that they are actually connected thanks to asynchrony (an important aspect not covered in Dardha and Pérez’s work); the connection is made precise by Theorem 76 and Corollary 77. Here again delayed actions in result to be insightful for an enhanced understanding of logic-based session types. In this line, we observe that De Young et al. [10] study asynchrony under “propositions-as-sessions”, and in particular explain the role of commuting conversions, which in an asynchronous setting act as as structural congruences (cf. Definition 40). In the synchronous case, they correspond to behavioral equivalences [30].
An interesting point concerns the exact relation between our class (Definition 34) and the class in Dardha and Pérez’s work. There is a key difference between the two: while they consider with a typing rule for independent parallel composition (cf. Rule H-Mix2 in Figure 5), we only have Rule C-Mix0 in Figure 4. The reason is technical: it is known that having both Mix0 and Mix2 induces the conflation of the units and , which conflicts with the distinction made by ’s denotational semantics (see [19] for details). (In [9], the conflated type is denoted “”, and there are no process constructs for session closing.) For the sake of consistency with the denotational semantics, we opted to not include this rule. Therefore, there are processes that are not in our class but are in Dardha and Pérez’s .
Having discovered the relation between DF and commuting conversions and disentanglement, an interesting item for future work is revisiting the process transformations proposed by Dardha and Pérez [9] using disentanglement. To focus on the fundamental issues of DF enforcement, we have not covered processes with recursion/sharing; we also plan to consider typed languages with constructs for shared servers and clients.
References
- [1] Stephanie Balzer, Bernardo Toninho, and Frank Pfenning. Manifest deadlock-freedom for shared session types. In Luís Caires, editor, Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, volume 11423 of Lecture Notes in Computer Science, pages 611–639. Springer, 2019. doi:10.1007/978-3-030-17184-1_22.
- [2] Gérard Boudol. Asynchrony and the -calculus (note). Technical report, Rapport de Recherche 1702, INRIA, Sophia-Antipolis, 1992.
- [3] Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In Paul Gastin and François Laroussinie, editors, CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings, volume 6269 of Lecture Notes in Computer Science, pages 222–236. Springer, 2010. doi:10.1007/978-3-642-15375-4_16.
- [4] Luís Caires and Bernardo Toninho. The session abstract machine. In Stephanie Weirich, editor, Programming Languages and Systems - 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I, volume 14576 of Lecture Notes in Computer Science, pages 206–235. Springer, 2024. doi:10.1007/978-3-031-57262-3_9.
- [5] Marco Carbone and Søren Debois. A graphical approach to progress for structured communication in web services. In Simon Bliudze, Roberto Bruni, Davide Grohmann, and Alexandra Silva, editors, Proceedings Third Interaction and Concurrency Experience: Guaranteed Interaction, ICE 2010, Amsterdam, The Netherlands, 10th of June 2010, volume 38 of EPTCS, pages 13–27, 2010. doi:10.4204/EPTCS.38.4.
- [6] Tzu-Chun Chen, Mariangiola Dezani-Ciancaglini, and Nobuko Yoshida. On the preciseness of subtyping in session types. In Olaf Chitil, Andy King, and Olivier Danvy, editors, Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, Kent, Canterbury, United Kingdom, September 8-10, 2014, pages 135–146. ACM, 2014. doi:10.1145/2643135.2643138.
- [7] Ornela Dardha and Simon J. Gay. A new linear logic for deadlock-free session-typed processes. In Christel Baier and Ugo Dal Lago, editors, Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, volume 10803 of Lecture Notes in Computer Science, pages 91–109. Springer, 2018. doi:10.1007/978-3-319-89366-2_5.
- [8] Ornela Dardha, Elena Giachino, and Davide Sangiorgi. Session types revisited. In Proc. of PPDP’12, pages 139–150. ACM, 2012. doi:10.1145/2370776.2370794.
- [9] Ornela Dardha and Jorge A. Pérez. Comparing type systems for deadlock freedom. Journal of Logical and Algebraic Methods in Programming, 124:100717, 2022. (Preliminary version in the Proceedings of EXPRESS/SOS 2015). doi:10.1016/j.jlamp.2021.100717.
- [10] Henry DeYoung, Luís Caires, Frank Pfenning, and Bernardo Toninho. Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication. In Patrick Cégielski and Arnaud Durand, editors, CSL, volume 16 of LIPIcs, pages 228–242. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2012. doi:10.4230/LIPICS.CSL.2012.228.
- [11] Mariangiola Dezani-Ciancaglini, Ugo de’Liguoro, and Nobuko Yoshida. On progress for structured communications. In Gilles Barthe and Cédric Fournet, editors, Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers, volume 4912 of Lecture Notes in Computer Science, pages 257–275. Springer, 2007. doi:10.1007/978-3-540-78663-4_18.
- [12] Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, and J. Garrett Morris. Separating sessions smoothly. In Serge Haddad and Daniele Varacca, editors, 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, volume 203 of LIPIcs, pages 36:1–36:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPICS.CONCUR.2021.36.
- [13] Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, and J. Garrett Morris. Separating sessions smoothly. Logical Methods in Computer Science, Volume 19, Issue 3, July 2023. doi:10.46298/lmcs-19(3:3)2023.
- [14] Simon J. Gay and Vasco Thudichum Vasconcelos. Linear type theory for asynchronous session types. J. Funct. Program., 20(1):19–50, 2010. doi:10.1017/S0956796809990268.
- [15] Silvia Ghilezan, Jovanka Pantović, Ivan Prokić, Alceste Scalas, and Nobuko Yoshida. Precise subtyping for asynchronous multiparty sessions. Proc. ACM Program. Lang., 5(POPL), January 2021. doi:10.1145/3434297.
- [16] Kohei Honda and Mario Tokoro. On asynchronous communication semantics. In Object-Based Concurrent Computing, number 612, in LNCS, 1992.
- [17] Keigo Imai, Rumyana Neykova, Nobuko Yoshida, and Shoji Yuen. Multiparty Session Programming With Global Protocol Combinators. In Robert Hirschfeld and Tobias Pape, editors, 34th European Conference on Object-Oriented Programming (ECOOP 2020), volume 166 of Leibniz International Proceedings in Informatics (LIPIcs), pages 9:1–9:30, Dagstuhl, Germany, 2020. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.ECOOP.2020.9.
- [18] Jules Jacobs and Stephanie Balzer. Higher-order leak and deadlock free locks. Proc. ACM Program. Lang., 7(POPL):1027–1057, 2023. doi:10.1145/3571229.
- [19] Juan C. Jaramillo and Jorge A. Pérez. Contrasting deadlock-free session processes (extended version), 2025. arXiv:2504.15845.
- [20] Naoki Kobayashi. TyPiCal: Type-based Static Analyzer for the Pi-Calculus. https://www-kb.is.s.u-tokyo.ac.jp/˜koba/typical/. Accessed: 2025-03-13.
- [21] Naoki Kobayashi. A new type system for deadlock-free processes. In CONCUR’06, volume 4137 of LNCS, pages 233–247, 2006. doi:10.1007/11817949_16.
- [22] Wen Kokke, Fabrizio Montesi, and Marco Peressotti. Taking linear logic apart. In Thomas Ehrhard, Maribel Fernández, Valeria de Paiva, and Lorenzo Tortora de Falco, editors, Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Linearity-TLLA@FLoC 2018, Oxford, UK, 7-8 July 2018, volume 292 of EPTCS, pages 90–103, 2018. doi:10.4204/EPTCS.292.5.
- [23] Wen Kokke, Fabrizio Montesi, and Marco Peressotti. Better late than never: A fully-abstract semantics for classical processes. Proceedings of the ACM on Programming Languages, 3(POPL), 2019. doi:10.1145/3290337.
- [24] Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types. In Karim Ali and Jan Vitek, editors, 36th European Conference on Object-Oriented Programming (ECOOP 2022), volume 222 of Leibniz International Proceedings in Informatics (LIPIcs), pages 4:1–4:29, Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.ECOOP.2022.4.
- [25] Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. Fencing off go: liveness and safety for channel-based programming. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 748–761. ACM, 2017. doi:10.1145/3009837.3009847.
- [26] Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. A static verification framework for message passing in go using behavioural types. In Michel Chaudron, Ivica Crnkovic, Marsha Chechik, and Mark Harman, editors, Proceedings of the 40th International Conference on Software Engineering, ICSE 2018, Gothenburg, Sweden, May 27 - June 03, 2018, pages 1137–1148. ACM, 2018. doi:10.1145/3180155.3180157.
- [27] Luca Padovani. Deadlock and lock freedom in the linear -calculus. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, New York, NY, USA, 2014. Association for Computing Machinery. doi:10.1145/2603088.2603116.
- [28] Luca Padovani. A simple library implementation of binary sessions. J. Funct. Program., 27:e4, 2017. doi:10.1017/S0956796816000289.
- [29] Luca Padovani and Luca Novara. Types for deadlock-free higher-order programs. In Susanne Graf and Mahesh Viswanathan, editors, Formal Techniques for Distributed Objects, Components, and Systems - 35th IFIP WG 6.1 International Conference, FORTE 2015, Held as Part of the 10th International Federated Conference on Distributed Computing Techniques, DisCoTec 2015, Grenoble, France, June 2-4, 2015, Proceedings, volume 9039 of Lecture Notes in Computer Science, pages 3–18. Springer, 2015. doi:10.1007/978-3-319-19195-9_1.
- [30] Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logical relations and observational equivalences for session-based concurrency. Information and Computation, 239:254–302, 2014. doi:10.1016/j.ic.2014.08.001.
- [31] Zesen Qian, G. A. Kavvos, and Lars Birkedal. Client-server sessions in linear logic. Proc. ACM Program. Lang., 5(ICFP), August 2021. doi:10.1145/3473567.
- [32] Davide Sangiorgi and David Walker. PI-Calculus: A Theory of Mobile Processes. Cambridge University Press, USA, 2001.
- [33] Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming. In Peter Müller, editor, 31st European Conference on Object-Oriented Programming (ECOOP 2017), volume 74 of Leibniz International Proceedings in Informatics (LIPIcs), pages 24:1–24:31, Dagstuhl, Germany, 2017. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.ECOOP.2017.24.
- [34] Bernardo Toninho and Nobuko Yoshida. Interconnectability of session-based logical processes. ACM Trans. Program. Lang. Syst., 40(4):17:1–17:42, 2018. doi:10.1145/3242173.
- [35] Bas van den Heuvel and Jorge A. Pérez. A gentle overview of asynchronous session-based concurrency: Deadlock freedom by typing. In Clément Aubert, Cinzia Di Giusto, Simon Fowler, and Violet Ka I Pun, editors, Proceedings 17th Interaction and Concurrency Experience, ICE 2024, Groningen, The Netherlands, 21st June 2024, volume 414 of EPTCS, pages 1–20, 2024. doi:10.4204/EPTCS.414.1.
- [36] Vasco T. Vasconcelos. Fundamentals of session types. Inf. Comput., 217:52–70, 2012. doi:10.1016/j.ic.2012.05.002.
- [37] Philip Wadler. Propositions as sessions. J. Funct. Program., 24(2-3):384–418, 2014. doi:10.1017/S095679681400001X.