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.

翻译：我们探讨了设计具有非确定性选择的类型化并发演算的问题，其中类型利用线性性来控制资源，从而确保进程具备强正确性性质。该问题受到非确定性与线性性之间微妙张力的制约。先前的研究开发了一种带有标准非确定性选择的会话类型化π-演算；良类型进程享有类型保持性和无死锁性。该类型化演算的核心是一种惰性语义，它逐步丢弃选择中的分支。然而，这种惰性语义较为复杂：需要多种技术要素来描述类型化进程的非确定性行为。本文提出了一种基于急切语义的全新方法，该方法能更直接地表示选择与提交行为。我们提出了一种π-演算，其中非确定性选择受此急切语义和会话类型共同约束。我们建立了其关键正确性性质（包括无死锁性），并通过正确翻译一个类型化资源λ-演算证明了其表达能力。