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 𝗌π.
@InProceedings{paulus_et_al:LIPIcs.TYPES.2021.11, author = {Paulus, Joseph W. N. and Nantes-Sobrinho, Daniele and P\'{e}rez, Jorge A.}, title = {{Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes}}, booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)}, pages = {11:1--11:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-254-9}, ISSN = {1868-8969}, year = {2022}, volume = {239}, editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.11}, URN = {urn:nbn:de:0030-drops-167808}, doi = {10.4230/LIPIcs.TYPES.2021.11}, annote = {Keywords: Resource \lambda-calculus, intersection types, session types, process calculi} }
Feedback for Dagstuhl Publishing