Comparing Session Type Systems derived from Linear Logic

TL;DR

The work formalizes a unifying πULL framework that ties session types to a concurrent fragment of Girard's Logic of Unity (LU) and uses it to compare session-type systems derived from classical and intuitionistic linear logic. By embedding both interpretations into πULL, the authors precisely characterize when intuitionistic typings (πILL) are included in or strictly contained within classical typings (πCLL^*), with πULL exactly capturing the classical class and strictly containing the intuitionistic one. They show locality and channel-connection implications of the two interpretations, demonstrating that locality is enforced by intuitionistic logic and that classical logic affords more expressive parallel composition and cycle rules. The results provide formal grounding for why classical linear logic-based session types are more permissive in typability, while intuitionistic interpretations enforce locality constraints, and they discuss the impact on deadlock-freedom, process composition, and potential extensions. Overall, the paper clarifies the landscape of logically grounded session-type systems and offers a solid framework for future exploration of mix-cycle extensions and practical typing discipline trade-offs.

Abstract

Session types are a typed approach to message-passing concurrency, where types describe sequences of intended exchanges over channels. Session type systems have been given strong logical foundations via Curry-Howard correspondences with linear logic, a resource-aware logic that naturally captures structured interactions. These logical foundations provide an elegant framework to specify and (statically) verify message-passing processes. In this paper, we rigorously compare different type systems for concurrency derived from the Curry-Howard correspondence between linear logic and session types. We address the main divide between these type systems: the classical and intuitionistic presentations of linear logic. Over the years, these presentations have given rise to separate research strands on logical foundations for concurrency; the differences between their derived type systems have only been addressed informally. To formally assess these differences, we develop $π\mathsf{ULL}$, a session type system that encompasses type systems derived from classical and intuitionistic interpretations of linear logic. Based on a fragment of Girard's Logic of Unity, $π\mathsf{ULL}$ provides a basic reference framework: we compare existing session type systems by characterizing fragments of $π\mathsf{ULL}$ that coincide with classical and intuitionistic formulations. We analyze the significance of our characterizations by considering the locality principle (enforced by intuitionistic interpretations but not by classical ones) and forms of process composition induced by the interpretations.

Figures (5)

• Figure 1: Structural congruence and reduction for $\pi\mathsf{ULL}$.
• Figure 2: The $\pi\mathsf{ULL}\xspace$ type system.
• Figure 3: Cut-rules of the $\pi\mathsf{ULL}$ type system.
• Figure 4: The $\pi\mathsf{ILL}$ type system.
• Figure 5: The $\pi\mathsf{CLL}\xspace^\star$ type system.

Theorems & Definitions (25)

• Definition 2.1
• Definition 2.2
• Definition 2.3
• Definition 2.4
• Definition 2.5
• Theorem 2.1: Subject Congruence
• proof : Proof (Sketch)
• Theorem 2.2: Subject Reduction
• proof : Proof (Sketch)
• Theorem 2.3: Progress