Joseph W. N. Paulus ; Daniele Nantes-Sobrinho ; Jorge A. Pérez - Non-Deterministic Functions as Non-Deterministic Processes (Extended Version)

lmcs:8812 - Logical Methods in Computer Science, October 10, 2023, Volume 19, Issue 4 - https://doi.org/10.46298/lmcs-19(4:1)2023
Non-Deterministic Functions as Non-Deterministic Processes (Extended Version)Article

Authors: Joseph W. N. Paulus ; Daniele Nantes-Sobrinho ; Jorge A. Pérez

    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.


    Volume: Volume 19, Issue 4
    Published on: October 10, 2023
    Accepted on: July 3, 2023
    Submitted on: December 8, 2021
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 872 times.
    This article's PDF has been downloaded 291 times.