Click here to flash read.
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 lambdafail, a new non-deterministic calculus in which
intersection types control resources (terms); on the concurrent side, we
consider spi, 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 lambdafail into spi and establish its correctness. Our
encoding precisely explains the interplay of non-deterministic and fail-prone
evaluation in lambdafail via typed processes in spi. In particular, it shows
how failures in sequential evaluation (absence/excess of resources) can be
neatly codified as interaction protocols.
No creative common's license