Non-Deterministic Functions as Non-Deterministic Processes (Extended Version)
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2021
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866914675866730496 |
|---|---|
| author | Paulus, Joseph W. N. Nantes-Sobrinho, Daniele Pérez, Jorge A. |
| author_facet | Paulus, Joseph W. N. Nantes-Sobrinho, Daniele Pérez, Jorge A. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2104_14759 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | Non-Deterministic Functions as Non-Deterministic Processes (Extended Version) Paulus, Joseph W. N. Nantes-Sobrinho, Daniele Pérez, Jorge A. Logic in Computer Science 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. |
| title | Non-Deterministic Functions as Non-Deterministic Processes (Extended Version) |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2104.14759 |