Typed Non-determinism in Functional and Concurrent Calculi
PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2023(2023)
摘要
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.
更多查看译文
关键词
concurrent calculi,functional,non-determinism
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要