We study functional and concurrent calculi with non-determinism, along with type systems to control resources based on linearity. The interplay between non-determinism and linearity is delicate: careless handling of branches can discard resources meant to be used exactly once. Here we go beyond prior work by considering non-determinism in its standard sense: once a branch is selected, the rest are discarded. Our technical contributions are three-fold. First, we introduce a $\pi$-calculus with non-deterministic choice, governed by session types. Second, we introduce a resource $\lambda$-calculus, governed by intersection types, in which non-determinism concerns fetching of resources from bags. Finally, we connect our two typed non-deterministic calculi via a correct translation.

翻译：我们研究了带有非确定性的函数式和并发演算，以及基于线性逻辑的资源控制类型系统。非确定性与线性逻辑之间的交互是微妙的：对分支的粗心处理可能会丢弃本应只使用一次的资源。本文超越了先前工作，考虑了非确定性的标准含义：一旦选择某个分支，其余分支即被丢弃。我们的技术贡献包含三个方面。首先，我们引入了一个由会话类型控制的带有非确定性选择的π演算。其次，我们引入了一个由交集类型控制的资源λ演算，其中非确定性涉及从包中获取资源。最后，我们通过一个正确的翻译将两个类型化非确定性演算联系起来。