English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Type-preserving translations are effective rigorous tools in the study ofcore programming calculi. In this paper, we develop a new typed translationthat connects sequential and concurrent calculi; it is governed by type systemsthat control resource consumption. Our main contribution is the sourcelanguage, 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 systembased on intersection types to control resources and fail-prone computation.The target language is \spi, an existing session-typed $\pi$-calculus thatresults from a Curry-Howard correspondence between linear logic and sessiontypes. Our typed translation subsumes our prior work; interestingly, it treatsunrestricted resources in \lamrfailunres as client-server session behaviours in\spi.

Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes (Extended Version)