Keywords

1 Introduction

Session types [29, 30, 47] are types for protocols. Regular types ensure functions are used according to their specification. Session types ensure communication channels are used according to their protocols. Session types have been studied in many settings. For instance, in the \(\pi \)-calculus [29, 30, 47], a foundational calculus for communication and concurrency, and in concurrent \(\lambda \)-calculi [26], including the focus of our paper: Good Variation [39, 54, GV].

GV is a concurrent \(\lambda \)-calculus with binary session types, where each channel is shared between exactly two processes. Binary session types guarantee two crucial properties communication safety—e.g., if the protocol says to transmit an integer, you transmit an integer—and session fidelity—e.g., if the protocol says send, you send. A third crucial property is deadlock freedom, which ensures that processes do not have cyclic dependencies—e.g., when two processes wait for each other to send a value. Binary session types alone are insufficient to rule out deadlocks arising from interleaved sessions, but several additional techniques have been developed to guarantee deadlock freedom in session-typed \(\pi \)-calculus and concurrent \(\lambda \)-calculus.

In the \(\pi \)-calculus literature, there have been several attempts at developing Curry-Howard correspondences between session-typed \(\pi \)-calculus and linear logic [27]: Caires and Pfenning’s \(\pi \)DILL [9] corresponds to dual intuitionistic linear logic [4], and Wadler’s Classical Processes [53, CP] corresponds to classical linear logic [27, CLL]. Both calculi guarantee deadlock freedom, which they achieve by restricting structure of processes and shared channels to trees, by combing name restriction and parallel composition into a single construct, corresponding to the logical cut. This ensures that two processes can only communicate via exactly one series of channels, which rules out interleavings of sessions, and guarantees deadlock freedom. There are many downsides to combining name restriction and parallel composition, such as lack of modularity, difficulty typing structural congruence and formulating label-transition semantics, which have led to various approaches to decoupling these constructs. Hypersequent CP [37, 38, 41] and Linear Compositional Choreographies [14] decouple them, but maintain the correspondence to CLL and allow only tree-structured processes. Priority CP [20, PCP] weakens the correspondence to CLL in exchange for a more expressive language which allows cyclic-structured processes. PCP decouples CP’s cut rule into two separate constructs: one for parallel composition via a mix rule, and one for name restriction via a cycle rule. To restore deadlock freedom, PCP uses priorities [34, 44]. Priorities encode the order of actions and rule out bad cyclic interleavings. Dardha and Gay [20] prove cycle-elimination for PCP, adapting the cut-elimination proof for classical linear logic, and deadlock freedom follows as a corollary.

CP and GV are related via a pair of translations which satisfy simulation [40], and which can be tweaked to satisfy reflection. The two calculi share the same strong guarantees. GV achieves deadlock freedom via a similar syntactic restriction: it combines channel creation and thread spawning into a single operation, called “fork”, which is related to the cut construct in CP. Unfortunately, as with CP, this syntactic restriction has its downsides.

Our aim is to develop a more expressive version of GV while maintaining deadlock freedom. While process calculi have their advantages, e.g., their succinctness, we chose to work with GV for several reasons. In general, concurrent \(\lambda \)-calculi support higher-order functions, and have a capability for abstraction not usually present in process calculi. Within a concurrent \(\lambda \)-calculus, one can derive extensions of the communication capabilities of the language via well-understood extensions of the functional fragment, e.g., we can derive internal/external choice from sum types. Concurrent \(\lambda \)-calculi maintain a clear separation between the program which the user writes and the configurations which represent the state of the system as it evaluates the program. However, our main motivation is that results obtained for \(\lambda \)-calculi transfer more easily to real-world functional programming languages. Case in point: we easily adapted the type system of PGV to Linear Haskell [6], which gives us a library for deadlock-free session-typed programming [36]. The benefit of working specifically with GV, as opposed to other concurrent \(\lambda \)-calculi, is its relation to CP [53], and its formal properties, including deadlock freedom. We thus pose our research question for GV:

RQ: Can we design a more expressive GV which guarantees deadlock freedom for cyclic-structured processes?

We follow the line of work from CP to Priority CP, and present Priority GV (PGV), a variant of GV which decouples channel creation from thread spawning, thus allowing cyclic-structured processes, but which nonetheless guarantees deadlock freedom via priorities. This closes the circle of the connection between CP and GV [53], and their priority-based versions, PCP [20] and PGV. We make the following main contributions:

  • (Sect. 2) Priority GV. We present Priority GV (Sect. 2, PGV), a session-typed functional language with priorities, and prove subject reduction (Theorem 1) and progress (Theorem 2). We addresses several problems in the original GV language, most notably: (a) PGV does not require the pseudo-type \(S^\sharp \); and (b) its structural congruence is type preserving. PGV answers our research question positively as it allows cyclic-structured binary session-typed processes that are deadlock free.

  • (Sect. 3) Translation from PCP to PGV. We present a sound and complete encoding of Priority CP [20] in PGV (Sect. 3). We prove the encoding preserves typing (Theorem 4) and satisfies operational correspondence (Theorems 5 and 6). To obtain a tight correspondence, we update PCP, moving away from commuting conversions and reduction as cut elimination towards reduction based on structural congruence, as it is standard in process calculi.

2 Priority GV

We present Priority GV (PGV), a session-typed functional language based on GV [39, 54] which uses priorities à la Kobayashi and Padovani [34, 45] to enforce deadlock freedom. Priority GV offers a more fine-grained analysis of communication structures, and by separating channel creation form thread spawning it allows cyclic structures. We illustrate this with two programs in PGV, examples 1 and 2. Each program contains two processes—the main process, and the child process created by —which communicate using two channels. The child process receives a unit over the channel , and then sends a unit over the channel . The main process does one of two things: (a) in example 1, it sends a unit over the channel , and then waits to receive a unit over the channel ; (b) in Example 2, it does these in the opposite order, which results in a deadlock. PGV is more expressive than GV: Example 1 is typeable and guaranteed deadlock-free in PGV, but is not typeable in GV [53] and not guaranteed deadlock-free in GV’s predecessor [26]. We believe PGV is a non-conservative extension of GV, as CP can be embedded in a Kobayashi-style system [22].

figure a

Session Types. Session types () are defined by the following grammar:

Session types and describe the endpoints of a channel over which we send or receive a value of type , and then proceed as . Types and describe endpoints of a channel whose communication has finished, and over which we must synchronise before closing the channel. Each connective in a session type is annotated with a priority .

Types. Types (, ) are defined by the following grammar:

Types , , , and are the standard linear \(\lambda \)-calculus product type, unit type, sum type, and empty type. Type is the standard linear function type, annotated with priority bounds . Every session type is also a type. Given a function with type , is a lower bound on the priorities of the endpoints captured by the body of the function, and is an upper bound on the priority of the communications that take place as a result of applying the function. The type of pure functions , i.e., those which perform no communications, is syntactic sugar for .

Environments. Typing environments , associate types to names. Environments are linear, so two environments can only be combined as if their names are distinct, i.e., .

Duality. Duality plays a crucial role in session types. The two endpoints of a channel are assigned dual types, ensuring that, for instance, whenever one program sends a value on a channel, the program on the other end is waiting to receive. Each session type has a dual, written . Duality is an involutive function which preserves priorities:

Priorities. Function returns the smallest priority of a session type. The type system guarantees that the top-most connective always holds the smallest priority, so we simply return the priority of the top-most connective:

We extend the function to types and typing contexts by returning the smallest priority in the type or context, or if there is no priority. We use \(\sqcap \) and \(\sqcup \) to denote the minimum and maximum:

Terms. Terms (, , ) are defined by the following grammar:

Let , , , and range over variable names. Occasionally, we use , , , and . The term language is the standard linear \(\lambda \)-calculus with products, sums, and their units, extended with constants for the communication primitives.

Constants are best understood in conjunction with their typing and reduction rules in Figs. 1 and 2. Briefly, links two endpoints together, forwarding messages from one to the other, creates a new channel and returns a pair of its endpoints, and spawns off its argument as a new thread. The and functions send and receive values on a channel. However, since the typing rules for PGV ensure the linear usage of endpoints, they also return a new copy of the endpoint to continue the session. The and functions close a channel. We use syntactic sugar to make terms more readable: we write in place of , in place of , and in place of . We recover as .

Internal and External Choice. Typically, session-typed languages feature constructs for internal and external choice. In GV, these can be defined in terms of the core language, by sending or receiving a value of a sum type [39]. We use the following syntactic sugar for internal () and external () choice and their units:

As the syntax for units suggests, these are the binary and nullary forms of the more common n-ary choice constructs and , which one may obtain generalising the sum types to variant types. For simplicity, we present only the binary and nullary forms.

Similarly, we use syntactic sugar for the term forms of choice, which combine sending and receiving with the introduction and elimination forms for the sum and empty types. There are two constructs for binary internal choice, expressed using the meta-variable which ranges over . As there is no introduction for the empty type, there is no construct for nullary internal choice:

Operational Semantics. Priority GV terms are evaluated as part of a configuration of processes. Configurations are defined by the following grammar:

Configurations (, , ) consist of threads , parallel compositions , and name restrictions . To preserve the functional nature of PGV, where programs return a single value, we use flags () to differentiate between the main thread, marked , and child threads created by , marked . Only the main thread returns a value. We determine the flag of a configuration by combining the flags of all threads in that configuration:

The use of for child threads [39] overlaps with the use of the meta-variable for priorities [20]. Both are used to annotate sequents: flags appear on the sequent in configuration typing, and priorities in term typing. To distinguish the two symbols, they are typeset in a different font and a different colour.

Values (, ), evaluation contexts (), thread evaluation contexts (), and configuration contexts () are defined by the following grammars:

Fig. 1.
figure 1

Operational semantics for PGV.

Full size image

We factor the reduction relation of PGV into a deterministic reduction on terms () and a non-deterministic reduction on configurations (), see Fig. 1. We write and for the transitive closures, and and for the reflexive-transitive closures.

Term reduction is the standard call-by-value, left-to-right evaluation for GV, and only deviates from reduction for the linear \(\lambda \)-calculus in that it reduces terms to values or ready terms waiting to perform a communication action.

Fig. 2.
figure 2

Typing rules for PGV.

Full size image

Configuration reduction resembles evaluation for a process calculus: E-Link, E-Send, and E-Close perform communications, E-LiftC allows reduction under configuration contexts, and E-LiftSC embeds a structural congruence \(\equiv \). The remaining rules mediate between the process calculus and the functional language: E-New and E-Spawn evaluate the and constructs, creating the equivalent configuration constructs, and E-LiftM embeds term reduction.

Structural congruence satisfies the following axioms: \(\textsc {SC-LinkSwap}\) allows swapping channels in the link process. \(\textsc {SC-ResLink}\) allows restriction to applied to link which is structurally equivalent to the terminated process, thus allowing elimination of unnecessary restrictions. \(\textsc {SC-ResSwap}\) allows swapping channels and \(\textsc {SC-ResComm}\) states that restriction is commutative. \(\textsc {SC-ResExt}\) is the standard scope extrusion rule. Rules \(\textsc {SC-ParNil}\), \(\textsc {SC-ParComm}\) and \(\textsc {SC-ParAssoc}\) state that parallel composition uses the terminated process as the neutral element; it is commutative and associative.

While our configuration reduction is based on the standard evaluation for GV, the increased expressiveness of PGV allows us to simplify the relation on two counts. (a) We decompose the construct. In GV, creates a new channel, spawns a child thread, and, when the child thread finishes, it closes the channel to its parent. In PGV, these are three separate operations: , , and . We no longer require that every child thread finishes by returning a terminated channel. Consequently, we also simplify the evaluation of the construct. Intuitively, evaluating causes a substitution: if we have a channel bound as , then replaces all occurrences of by . However, in GV, is required to return a terminated channel, which means that the semantics for must create a fresh channel of type . The endpoint of type is returned by the construct, and a on the other endpoint guards the actual substitution. In PGV, evaluating simply causes a substitution. (b) Our structural congruence is type preserving. Consequently, we can embed it directly into the reduction relation. In GV, this is not the case, and subject reduction relies on proving that if ends up in an ill-typed configuration, we can rewrite it to a well-typed configuration using \(\equiv \).

Typing. Figure 2 gives the typing rules for PGV. Typing rules for terms are at the top of Fig. 2. Terms are typed by a judgement stating that “a term has type and an upper bound on its priority under the typing environment ”. Typing for the linear \(\lambda \)-calculus is standard. Linearity is ensured by splitting environments on branching rules, requiring that the environment in the variable rule consists of just the variable, and the environment in the constant and unit rules are empty. Constants are typed using type schemas, and embedded using T-Const (mid of Fig. 2). The typing rules treat all variables as linear resources, even those of non-linear types such as . However, the rules can easily be extended to allow values with unrestricted usage [53].

The only non-standard feature of the typing rules is the priority annotations. Priorities are based on obligations/capabilities used by Kobayashi [34], and simplified to single priorities following Padovani [44]. The integration of priorities into GV is adapted from Padovani and Novara [45]. Paraphrasing Dardha and Gay [20], priorities obey the following two laws: (i) an action with lower priority happens before an action with higher priority; and (ii) communication requires equal priorities for dual actions.

In PGV, we keep track of a lower and upper bound on the priorities of a term, i.e., while evaluating the term, when does it start communicating, and when does it finish. The upper bound is written on the sequent, whereas the lower bound is approximated from the typing environment. Typing rules for sequential constructs enforce sequentially, e.g., the typing for has a side condition which requires that the upper bound of is smaller than the lower bound of , i.e., finishes before starts. The typing rule for ensures that both endpoints of a channel share the same priorities. Together, these two constraints guarantee deadlock freedom.

To illustrate this, let’s go back to the deadlocked program in Example 2. Crucially, it composes the terms below in parallel. While each of these terms itself is well-typed, they impose opposite conditions on the priorities, so their composition is ill-typed. (We omit the priorities on and .)

figure b

Closures suspend communication, so T-Lam stores the priority bounds of the function body on the function type, and T-App restores them. For instance, is assigned the type , i.e., a function which, when applied, starts and finishes communicating at priority .

figure c

Typing rules for configurations are at the bottom of Fig. 2. Configurations are typed by a judgement stating that “a configuration with flag \(\phi \) is well typed under typing environment ”. Configuration typing is based on the standard typing for GV. Terms are embedded either as main or as child threads. The priority bound from the term typing is discarded, as configurations contain no further blocking actions. Main threads are allowed to return a value, whereas child threads are required to return the unit value. Sequents are annotated with a flag \(\phi \), which ensures that there is at most one main thread.

While our configuration typing is based on the standard typing for GV, it differs on two counts: (i) we require that child threads return the unit value, as opposed to a terminated channel; and (ii) we simplify typing for parallel composition. In order to guarantee deadlock freedom, in GV each parallel composition must split exactly one channel of the channel pseudo-type into two endpoints of type and . Consequently, associativity of parallel composition does not preserve typing. In PGV, we guarantee deadlock freedom using priorities, which removes the need for the channel pseudo-type , and simplifies typing for parallel composition, while restoring type preservation for the structural congruence.

Subject Reduction. Unlike with previous versions of GV, structural congruence, term reduction, and configuration reduction are all type preserving.

We must show that substitution preserves priority constraints. For this, we prove Lemma 1, which shows that values have finished all their communication, and that any priorities in the type of the value come from the typing environment.

Lemma 1

If , then , and .

Lemma 2

(Substitution).

If and , then .

Lemma 3

(Subject Reduction, ).

If and , then .

Lemma 4

(Subject Congruence, \(\equiv \) ).

If and , then .

Theorem 1

(Subject Reduction, ).

If and , then .

Progress and Deadlock Freedom. PGV satisfies progress, as PGV configurations either reduce or are in normal form. However, the normal forms may seem surprising at first, as evaluating a well-typed PGV term does not necessarily produce just a value. If a term returns an endpoint, then its normal form contains a thread which is ready to communicate on the dual of that endpoint. This behaviour is not new to PGV. Let us consider an example, adapted from Lindley and Morris [39], in which a term returns an endpoint linked to an echo server. The echo server receives a value and sends it back unchanged. Consider the program which creates a new channel, with endpoints and , spawns off an echo server listening on , and then returns :

figure d

If we reduce the above program, we get . Clearly, no more evaluation is possible, even though the configuration contains the thread , which is blocked on . In Corollary 1 we will show that if a term does not return an endpoint, it must produce only a value.

Actions are terms which perform communication actions and which synchronise between two threads. Ready terms are terms which perform communication actions, either by themselves, e.g., creating a new channel or thread, or with another thread, e.g., sending or receiving. Progress for the term language is standard for GV, and deviates from progress for linear \(\lambda \)-calculus only in that terms may reduce to values or ready terms:

Definition 1

(Actions). A term acts on an endpoint if it is , , , or . A term is an action if it acts on some endpoint .

Definition 2

(Ready Terms). A term is ready if it is of the form , where is of the form , , , or acts on . In the latter case, we say that is ready to act on .

Lemma 5

(Progress, ). If and contains only session types, then: (a) is a value; (b) for some ; or (c) is ready.

Canonical forms deviate from those for GV, in that we opt to move all \(\nu \)-binders to the top. The standard GV canonical form, alternating \(\nu \)-binders and their corresponding parallel compositions, does not work for PGV, since multiple channels may be split across a single parallel composition.

A configuration either reduces, or it is equivalent to configuration in normal form. Crucial to the normal form is that each term is blocked on the corresponding channel , and hence no two terms act on dual endpoints. Furthermore, no term can perform a communication action by itself, since those are excluded by the definition of actions. Finally, as a corollary, we get that well-typed terms which do not return endpoints return just a value:

Definition 3

(Canonical Forms). A configuration is in canonical form if it is of the form where no term is a value.

Lemma 6

(Canonical Forms). If , there exists some such that and is in canonical form.

Definition 4

(Normal Forms). A configuration is in normal form if it is of the form where each is ready to act on .

Theorem 2

(Progress, ). If and is in canonical form, then either for some ; or for some in normal form.

Proof

(Sketch). Our proof follows that of Kobayashi [34, theorem 2]. We apply Lemma 5 to each thread. Either we obtain a reduction, or each child thread is ready and the main thread ready or a value. We pick the ready term with the smallest priority bound. If contains new, spawn, or a link, we apply E-New, E-Spawn, or E-Link. Otherwise, must be ready on some . Linearity guarantees there is some thread which acts on . If is ready, priority typing guarantees it is ready on , and we apply E-Send or E-Close. If is not ready, it must be the main thread returning a value. We move into the \(i^{\text {th}}\) position and repeat until we either find a reduction or reach normal form.

Corollary 1

If , , and contains no endpoints, then for some value .

It follows immediately from Theorem 2 and Corollary 1 that a term which does not return an endpoint will complete all its communication actions, thus satisfying deadlock freedom.

3 Relation to Priority CP

We present a correspondence between Priority GV and an updated version of Priority CP [20, PCP], which is Wadler’s CP [53] with priorities. This correspondence connects PGV to (a relaxed variant of) classical linear logic.

3.1 Revisiting Priority CP

Types. (, ) in PCP correspond to linear logic connectives annotated with priorities . Typing environments, duality, and the priority function are defined as expected.

Processes. (, ) in PCP are defined by the following grammar.

Processes are typed by sequents , which correspond to the one-sided sequents in classical linear logic. Differently from PGV, in PCP we do not need to store the greatest priority on the sequent, as, due to the absence of higher-order functions, we cannot compose processes sequentially.

PCP decomposes cut into T-Res and T-Par rules—corresponding to cycle and mix rules, respectively—and guarantees deadlock freedom by using priority constraints, e.g.,, as in T-Send.

figure e

The main change we make to PCP is removing commuting conversions and defining an operational semantics based on structural congruence. Commuting conversions are necessary if we want our reduction strategy to correspond exactly to cut elimination. However, from the perspective of process calculi, commuting conversions behave strangely: they allow an input/output action to be moved to the top of a process, thus potentially blocking actions which were previously possible. This makes CP, and Dardha and Gay’s PCP [20], non-confluent. As Lindley and Morris [39] show, all communications that can be performed with the use of commuting conversions, can also be performed without them, using structural congruence.

In particular for PCP, commuting conversions break our intuition that an action with lower priority occurs before an action with higher priority. To cite Dardha and Gay [20] “if a prefix on a channel endpoint with priority is pulled out at top level, then to preserve priority constraints in the typing rules [..], it is necessary to increase priorities of all actions after the prefix on ” by . One benefit of removing commuting conversions is that we no longer need to dynamically change the priorities during reduction, which means that the intuition for priorities holds true in our updated version of PCP. Furthermore, we can safely define reduction on untyped processes, which means that type and priority information is erasable!

We prove closed progress for our updated PCP.

Theorem 3

(Progress, \(\Longrightarrow \)). If , then either or there exists a such that .

3.2 Correspondence Between PGV and PCP

We illustrate the relation between PCP and PGV by defining a translation from PCP to PGV. The translation on types is defined as follows:

There are two separate translations on processes. The main translation, , translates processes to terms:

Unfortunately, the operational correspondence along is unsound, as it translates \(\nu \)-binders and parallel compositions to and , which can reduce to their equivalent configuration constructs using E-New and E-Spawn. The same goes for \(\nu \)-binders which are inserted when translating bound send to unbound send. For instance, the process is blocked, but its translation uses and can reduce. To address this issue, we use a second translation, , which is equivalent to followed by reductions using E-New and E-Spawn:

Typing environments are translated pointwise, and sequents are translated as , where indicates a child thread. Translated processes do not have a main thread. The translations and preserve typing, and the latter induces a sound and complete operational correspondence.

Lemma 7

(Preservation, ). If , then .

Theorem 4

(Preservation, ). If , then .

Lemma 8

For any , either:

  • ; or

  • , and for any , if , then .

Theorem 5

(Operational Correspondence, Soundness, ). If and , there exists a such that and .

Theorem 6

(Operational Correspondence, Completeness, ). If and , then .

4 Related Work and Discussion

Deadlock Freedom and Progress. Deadlock freedom and progress are well studied properties in the \(\pi \)-calculus. For the ‘standard’ typed \(\pi \)-calculus, an important line of work starts from Kobayashi’s approach to deadlock freedom [33], where priorities are values from an abstract poset. Kobayashi [34] simplifies the abstract poset to pairs of naturals, called obligations andcapabilities. Padovani simplifies these further to a single natural, called a priority [44], and adapts obligations/capabilities to session types [43].

For the session-typed \(\pi \)-calculus, Dezani et al. [25] guarantee progress by allowing only one active session at a time. Dezani [24] introduces a partial order on channels, similar to Kobayashi [33]. Carbone and Debois [11] define progress for session typed \(\pi \)-calculus in terms of a catalyser which provides the missing counterpart to a process. Carbone et al. [10] use catalysers to show that progress is a compositional form of lock-freedom and can be lifted to session types via the encoding of session types to linear types [18, 21, 35]. Vieira and Vasconcelos [51] use single priorities and an abstract partial order to guarantee deadlock freedom in a binary session-typed \(\pi \)-calculus and building on conservation types.

While our work focuses on binary session types, it is worth to discuss related work on Multiparty Session Types (MPST). The line of work on MPST starts with Honda et al. [31], which guarantees deadlock freedom within a single session, but not for session interleaving. Bettini et al. [7] follow a technique similar to Kobayashi’s for MPST. The main difference with our work is that we associate priorities with communication actions, where Bettini et al. [7] associate them with channels. Carbone and Montesi [13] combine MPST with choreographies and obtain a formalism that satisfies deadlock freedom. Deniélou and Yoshida [23] introduce multiparty compatibility which generalises duality in binary session types. They synthesise safe and deadlock-free global types from local types leveraging LTSs and communicating automata. Castellani et al. [16] guarantee lock freedom, a stronger property than deadlock freedom, for MPST with internal delegation, where participants in the same session are allowed to delegate tasks to each other, and internal delegation is captured by the global type. Scalas and Yoshida [46] provide a revision of the foundations for MPST, and offer a less complicated and more general theory, by removing duality/consistency. The type systems is parametric and type checking is decidable, but allows for a novel integration of model checking techniques. More protocols and processes can be typed and are guaranteed to be free of deadlocks.

Neubauer and Thiemann [42] and Vasconcelos et al. [49, 50] introduce the first functional language with session types. Such works did not guarantee deadlock freedom until GV [39, 53]. Toninho et al. [48] present a translation of simply-typed \(\lambda \)-calculus into session-typed \(\pi \)-calculus, but their focus is not on deadlock freedom.

Ties with Logic. The correspondence between logic and types lays the foundation for functional programming [54]. Since its inception by Girard [27], linear logic has been a candidate for a foundational correspondence for concurrent programs. A correspondence with linear \(\pi \)-calculus was established early on by Abramsky [1] and Bellin and Scott [5]. Many years later, several correspondences between linear logic and the \(\pi \)-calculus with binary session types were proposed. Caires and Pfenning [9] propose a correspondence with dual intuitionistic linear logic, while Wadler [53] proposes a correspondence with classical linear logic. Both guarantee deadlock freedom as a consequence of cut elimination. Dardha and Gay [20] integrate Kobayashi and Padovani’s work on priorities [34, 44] with CP, loosening its ties to linear logic in exchange for expressivity. Dardha and Pérez [22] compare priorities à la Kobayashi with tree restrictions à la CP, and show that the latter is a subsystem of the former. Balzer et al. [2] introduce sharing at the cost of deadlock freedom, which they restore using an approach similar to priorities [3]. Carbone et al. [12, 15] give a logical view of MPST with a generalised duality. Caires and Pérez [8] give a presentation of MPST in terms of binary session types and the use of a medium process which guarantee protocol fidelity and deadlock freedom. Their binary session types are rooted in linear logic. Ciobanu and Horne [17] give the first Curry-Howard correspondence between MPST and BV [28], a conservative extension of linear logic with a non-commutative operator for sequencing. Horne [32] give a system for subtyping and multiparty compatibility where compatible processes are race free and deadlock free using a Curry-Howard correspondence, similar to the approach in [17].

Conclusion. We answered our research question by presenting Priority GV, a session-typed functional language which allows cyclic communication structures and uses priorities to ensure deadlock freedom. We showed its relation to Priority CP [20] via an operational correspondence.

Future Work. Our formalism so far only captures the core of GV. In future work, we plan to explore recursion, following Lindley and Morris [40] and Padovani and Novara [45], and sharing, following Balzer and Pfenning [2] or Voinea et al. [52].