Typed Non-determinism in Functional and Concurrent Calculi
Abstract
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 -calculus with non-deterministic choice, governed by session types. Second, we introduce a resource -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.
Keywords
Cite
@article{arxiv.2205.00680,
title = {Typed Non-determinism in Functional and Concurrent Calculi},
author = {Bas van den Heuvel and Joseph W. N. Paulus and Daniele Nantes-Sobrinho and Jorge A. Pérez},
journal= {arXiv preprint arXiv:2205.00680},
year = {2023}
}