Typed Non-determinism in Concurrent Calculi: The Eager Way

TL;DR

This work introduces an eagerly committing semantics for a session-typed π-calculus with non-deterministic choice, aligning non-determinism with linear resource control. It extends prior lazy-semantics foundations by providing a simpler operational model for reductions while preserving type preservation and deadlock-freedom under the eager rules. The paper also develops a resource λ-calculus with unrestricted resources (λ_C) and proves subject reduction/expansion within an intersection-type framework, then encodes λ_C into the eagerly semantics of ${\mathsf{s}\pi^{!}}$ and analyzes static and dynamic correctness. A comparative study between lazy and eager semantics via behavioral equivalences demonstrates both the strengths and limitations of each approach, highlighting that eager semantics can yield looser dynamic correspondences but offers simpler reasoning and practical expressivity. Overall, the work advances resource-sensitive concurrency by providing a clearer eager framework that remains faithful to session-type discipline and supports meaningful translations from resource-aware λ-calculi.

Abstract

We consider the problem of designing typed concurrent calculi with non-deterministic choice in which types leverage linearity for controlling resources, thereby ensuring strong correctness properties for processes. This problem is constrained by the delicate tension between non-determinism and linearity. Prior work developed a session-typed π-calculus with standard non-deterministic choice; well-typed processes enjoy type preservation and deadlock-freedom. Central to this typed calculus is a lazy semantics that gradually discards branches in choices. This lazy semantics, however, is complex: various technical elements are needed to describe the non-deterministic behavior of typed processes. This paper develops an entirely new approach, based on an eager semantics, which more directly represents choices and commitment. We present a π-calculus in which non-deterministic choices are governed by this eager semantics and session types. We establish its key correctness properties, including deadlock-freedom, and demonstrate its expressivity by correctly translating a typed resource λ-calculus.

Figures (10)

• Figure 1: ${{\mathsf{s}\pi\mkern-1mu}^{!}\mkern-1mu}$: syntax (top) and structural congruence (bottom).
• Figure 2: Eager reduction semantics for spi+.
• Figure 3: Typing rules for ${{\mathsf{s}\pi\mkern-1mu}^{!}\mkern-1mu}$.
• Figure 4: Syntax of $\lambda_{\mathtt{C}}\xspace$.
• Figure 5: Reduction rules for lambda.

Theorems & Definitions (17)

• definition 1
• definition 2
• theorem 1: Type Preservation
• theorem 2: Deadlock-freedom
• definition 3: $\eta \sim \epsilon$
• definition 4: Well-formedness in $\lambda_{\mathtt{C}}\xspace$
• theorem 3: SR in $\lambda_{\mathtt{C}}\xspace$
• theorem 4: SE in $\lambda_{\mathtt{C}}\xspace$
• definition 5
• theorem 5: Type Preservation