Non-deterministic functions as non-deterministic processes
Presented at the 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021 (July 2021), Virtual, Buenos Aires
We study encodings of the λ-calculus into the π-calculus in the unexplored case of calculi with non-determinism and failures. On the sequential side, we consider λ^↯_⊕, a new non-deterministic calculus in which intersection types control resources (terms); on the concurrent side, we consider sπ, a π-calculus in which non-determinism and failure rest upon a Curry-Howard correspondence between linear logic and session types. We present a typed encoding of λ^↯_⊕ into sπ and establish its correctness. Our encoding precisely explains the interplay of non-deterministic and fail-prone evaluation in λ^↯_⊕ via typed processes in sπ. In particular, it shows how failures in sequential evaluation (absence/excess of resources) can be neatly codified as interaction protocols.
|, , , ,|
|Leibniz International Proceedings in Informatics|
|6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021|
|Organisation||Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands|
Paulus, J.W.N, Nantes, D, & Pérez Parra, J.A. (2021). Non-deterministic functions as non-deterministic processes. In International Conference on Formal Structures for Computation and Deduction (pp. 21:1–21:22). doi:10.4230/LIPIcs.FSCD.2021.21