Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes (Extended Version)
share
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 expressive type systems that control resource consumption. Our main contribution is the source language, a new resource λ-calculus with non-determinism and failures, dubbed . In , resources are sharply separated into linear and unrestricted; failures are explicit and arise following this separation. We equip with a type system based on non-idempotent intersection types, which controls resources and fail-prone computation. The target language is an existing session-typed π-calculus, sπ, which results from a Curry-Howard correspondence between linear logic and session types for concurrency. Our typed translation of into sπ subsumes our prior work; interestingly, it elegantly treats unrestricted resources in as client-server session behaviors in sπ.
READ FULL TEXT