一句话：提出 lambdafail 到 spi 的带类型编码，用会话类型刻画非确定与失败求值的对应。
论文研究带非确定性与失败的计算中，lambda 演算到 pi 演算的编码问题。顺序侧提出 lambdafail：一种新的非确定 lambda 演算，用交集类型控制项所需资源；并发侧采用 spi：一种 pi 演算，其非确定性与失败建立在线性逻辑与会话类型之间的 Curry-Howard 对应上。作者给出从 lambdafail 到 spi 的带类型编码，并证明其正确性。该编码说明顺序求值中的失败（资源缺失或过剩）可被精确编码为进程间的交互协议，从而揭示非确定且可能失败的计算与带类型并发进程之间的结构对应。
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.
@article{paperbot2193,
title = {Non-Deterministic Functions as Non-Deterministic Processes (Extended Version)},
author = {Joseph W. N. Paulus and Daniele Nantes-Sobrinho and Jorge A. Pérez},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 4},
year = {2023},
doi = {10.46298/lmcs-19(4:1)2023}
}