Non-Deterministic Functions as Non-Deterministic Processes (Extended Version)

We study encodings of the lambda-calculus into the pi-calculus in theunexplored case of calculi with non-determinism and failures. On the sequentialside, we consider lambdafail, a new non-deterministic calculus in whichintersection types control resources (terms); on the concurrent side, weconsider spi, a pi-calculus in which non-determinism and failure rest upon aCurry-Howard correspondence between linear logic and session types. We presenta typed encoding of lambdafail into spi and establish its correctness. Ourencoding precisely explains the interplay of non-deterministic and fail-proneevaluation in lambdafail via typed processes in spi. In particular, it showshow failures in sequential evaluation (absence/excess of resources) can beneatly codified as interaction protocols