2026-07-23T08:19:38Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16780 2024-03-06T10:58:15Z ddc:004 open_access

Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes Paulus, Joseph W. N. Nantes-Sobrinho, Daniele Pérez, Jorge A. Resource λ-calculus intersection types session types process calculi 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 λ-calculus with non-collapsing non-determinism and failures, dubbed uλ^{↯}_{⊕}. In uλ^{↯}_{⊕}, 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 𝗌π, an existing session-typed π-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 uλ^{↯}_{⊕} as client-server session behaviours in 𝗌π. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Joseph W. N. Paulus and Daniele Nantes-Sobrinho and Jorge A. Pérez 2022 Is Part Of LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2021.11 urn:nbn:de:0030-drops-167808 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.11 eng https://creativecommons.org/licenses/by/4.0/legalcode