Type-preserving translations are effective rigorous tools in the study of core programming calculi. In this paper, we develop a new typed translation that connects sequential and concurrent calculi; it is governed by type systems that control resource consumption. Our main contribution is the source language, a new resource $\lambda$-calculus with non-determinism and failures, dubbed \ulamf. In \ulamf, resources are split into linear and unrestricted; failures are explicit and arise from this distinction. We define a type system based on intersection types to control resources and fail-prone computation. The target language is \spi, an existing session-typed $\pi$-calculus that results from a Curry-Howard correspondence between linear logic and session types. Our typed translation subsumes our prior work; interestingly, it treats unrestricted resources in \lamrfailunres as client-server session behaviours in \spi.
翻译:类型保存翻译是研究核心编程计算法的有效严格工具。 在本文中, 我们开发了一种新的打印翻译, 将相继和同时的计算法连接起来; 由控制资源消耗的类型系统管理。 我们的主要贡献是源语言, 一种新的资源 $ lambda$- 计算法, 带有非确定性和失败, 称为 ulamf 。 在 ulamf 中, 资源被分割成线性和非限制性; 失败是显而易见的, 并由此区分产生。 我们定义了一种基于交叉类型来控制资源和易失常计算的方法。 目标语言是\ spi, 一种现有的会话型 $\ pi$- 计算法, 由线性逻辑类型和会话类型之间的“ urry- Howard ” 对应产生。 我们的打字翻译分包将我们先前的工作; 有趣的是, 它将\lamrfailuns 中的不受限制的资源作为\ lamfailuns 客户- 服务器会话行为处理 。