Non-deterministic functions as non-deterministic processes (extended version)
File(s)2104.14759.pdf (1.72 MB)
Published version
Author(s)
Paulus, Joseph WN
Nantes-Sobrinho, Daniele
Pérez, Jorge A
Type
Journal Article
Abstract
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.
Date Issued
2023
Date Acceptance
2023-07-03
Citation
Logical Methods in Computer Science, 2023, 19 (4)
ISSN
1860-5974
Publisher
Logical Methods in Computer Science e.V.
Journal / Book Title
Logical Methods in Computer Science
Volume
19
Issue
4
Copyright Statement
© J. Paulus, D. Nantes, and J.A. Pérez Licence: Attribution 4.0 International (CC BY 4.0)
License URL
Identifier
http://dx.doi.org/10.46298/lmcs-19(4:1)2023
Publication Status
Published
Article Number
1
Date Publish Online
2023-10-10