Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes

Joseph W. N. Paulus, Daniele Nantes-Sobrinho, Jorge A. Pérez

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Abstract

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 𝗌π.
Original languageEnglish
Title of host publication27th International Conference on Types for Proofs and Programs (TYPES 2021)
EditorsHenning Basold, Jesper Cockx, Silvia Ghilezan
PublisherSchloss Dagstuhl--Leibniz-Zentrum für Informatik
Pages11.1-11.24
Number of pages24
ISBN (Print)978-3-95977-254-9
DOIs
Publication statusPublished - 4-Aug-2022

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
PublisherSchloss Dagstuhl--Leibniz-Zentrum für Informatik
Volume239
ISSN (Print)1868-8969

Cite this