2022/05/02 by Bas van den Heuvel, Heuvel, Bas van den, Joseph W. N. Paulus +5
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2205.00680
openalex publication_date 2022/05/02 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.