NON-DETERMINISTIC FUNCTIONS AS NON-DETERMINISTIC PROCESSES

We study encodings of the lambda-calculus into the pi-calculus in the unexplored case of calculi with non-determinism and failures. On the sequential side, we consider lambda((sic))(circle plus), a new non-deterministic calculus in which intersection types control resources (terms); on the concurrent side, we consider s pi, a pi-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 lambda((sic))(circle plus) into s pi and establish its correctness. Our encoding precisely explains the interplay of non-deterministic and fail-prone evaluation in lambda((sic) )(circle plus)via typed processes in s pi. In particular, it shows how failures in sequential evaluation (absence/excess of resources) can be neatly codified as interaction protocols.