2026-07-22T16:58:04Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9568 2024-03-06T10:44:44Z ddc:004 open_access

A Universal Session Type for Untyped Asynchronous Communication Balzer, Stephanie Pfenning, Frank Toninho, Bernardo Session types sharing pi-calculus bisimulation In the simply-typed lambda-calculus we can recover the full range of expressiveness of the untyped lambda-calculus solely by adding a single recursive type U = U -> U. In contrast, in the session-typed pi-calculus, recursion alone is insufficient to recover the untyped pi-calculus, primarily due to linearity: each channel just has two unique endpoints. In this paper, we show that shared channels with a corresponding sharing semantics (based on the language SILL_S developed in prior work) are enough to embed the untyped asynchronous pi-calculus via a universal shared session type U_S. We show that our encoding of the asynchronous pi-calculus satisfies operational correspondence and preserves observable actions (i.e., processes are weakly bisimilar to their encoding). Moreover, we clarify the expressiveness of SILL_S by developing an operationally correct encoding of SILL_S in the asynchronous pi-calculus. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Stephanie Balzer and Frank Pfenning and Bernardo Toninho 2018 Is Part Of LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2018.30 urn:nbn:de:0030-drops-95681 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.30 eng https://creativecommons.org/licenses/by/3.0/legalcode