Non-Deterministic Functions as Non-Deterministic Processes

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 ??, 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 ?? and establish its correctness. Our encoding precisely explains the interplay of non-deterministic and fail-prone evaluation in ?^?_? via typed processes in ??. In particular, it shows how failures in sequential evaluation (absence/excess of resources) can be neatly codified as interaction protocols