Prioritise the Best Variation

TL;DR

This work extends GV with a priority-based type system (PGV) to admit cyclic-structured, deadlock-free processes by decoupling channel creation from thread spawning and enforcing ordering via priorities. It proves subject reduction and progress for PGV, showing deadlock freedom in all well-typed configurations, and to connect with prior work it provides a sound and complete encoding of PCP into PGV while adjusting PCP to fit the PGV framework. The paper also demonstrates PGV's expressiveness through Milner's cyclic scheduler and details the PCP↔PGV correspondence through two translations, preserving typing and operational behavior. Overall, PGV advances the expressivity of session-typed functional languages while maintaining strong safety guarantees, bridging GV and PCP and offering practical pathways to embedding deadlock-free session-typed programming in real languages.

Abstract

Binary session types guarantee communication safety and session fidelity, but alone they cannot rule out deadlocks arising from the interleaving of different sessions. In Classical Processes (CP)$-$a process calculus based on classical linear logic$-$deadlock freedom is guaranteed by combining channel creation and parallel composition under the same logical cut rule. Similarly, in Good Variation (GV)$-$a linear concurrent $λ$-calculus$-$deadlock freedom is guaranteed by combining channel creation and thread spawning under the same operation, called fork. In both CP and GV, deadlock freedom is achieved at the expense of expressivity, as the only processes allowed are tree-structured. Dardha and Gay define Priority CP (PCP), which allows cyclic-structured processes and restores deadlock freedom by using priorities, in line with Kobayashi and Padovani. Following PCP, we present Priority GV (PGV), a variant of GV which decouples channel creation from thread spawning. Consequently, we type cyclic-structured processes and restore deadlock freedom by using priorities. We show that our type system is sound by proving subject reduction and progress. We define an encoding from PCP to PGV and prove that the encoding preserves typing and is sound and complete with respect to the operational semantics.

Figures (14)

• Figure 1: Operational Semantics for PGV.
• Figure 2: Typing Rules for PGV.
• Figure 3: Typing Rules for Syntactic Sugar for PGV (T-LamUnit, T-LamPair, T-Let, and T-Fork).
• Figure 4: Typing Rules for Syntactic Sugar for PGV (T-Select-Inl and T-Select-Inr).
• Figure 5: Typing Rules for Syntactic Sugar for PGV (T-Offer and T-Offer-Absurd).

Theorems & Definitions (33)

• Example 2.1
• Example 2.2
• Lemma 3.1
• Lemma 3.2
• Lemma 3.3
• Lemma 3.4
• Theorem 3.5
• Definition 3.6
• Definition 3.7
• Lemma 3.8