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.
, , , ,
doi.org/10.4230/LIPIcs.FSCD.2021.21
Leibniz International Proceedings in Informatics
6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021
Centrum Wiskunde & Informatica, Amsterdam, 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