Non-Deterministic Functions as Non-Deterministic Processes

Joseph W.N. Paulus, Daniele Nantes-Sobrinho, Jorge A. Pérez

OnderzoeksoutputAcademicpeer review

3 Downloads (Pure)


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.
Originele taal-2English
Titel6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)
RedacteurenNaoki Kobayashi
UitgeverijSchloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany
Aantal pagina's22
StatusPublished - 6-jul-2021

Citeer dit