Typed Non-determinism in Concurrent Calculi: The Eager Way

TL;DR

This paper introduces an eager semantics for typed non-deterministic choice in concurrent calculi, simplifying the representation of choices while ensuring deadlock-freedom and resource correctness.

Contribution

It proposes a new eager semantics approach for session-typed calculi, improving clarity and correctness over previous lazy semantics methods.

Findings

Proves deadlock-freedom of the new calculus

Shows expressivity by translating typed resource lambda-calculus

Demonstrates simpler, more direct semantics for non-determinism

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 {\pi}-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 {\pi}-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 {\lambda}-calculus.