Non-Deterministic Functions as Non-Deterministic Processes

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

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

3 Downloads (Pure)

Abstract

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.
Original languageEnglish
Title of host publication6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)
EditorsNaoki Kobayashi
PublisherSchloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany
Number of pages22
DOIs
Publication statusPublished - 6-Jul-2021

Cite this