eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-08-31
30:1
30:18
10.4230/LIPIcs.CONCUR.2018.30
article
A Universal Session Type for Untyped Asynchronous Communication
Balzer, Stephanie
1
Pfenning, Frank
1
Toninho, Bernardo
2
Carnegie Mellon University, USA
NOVA LINCS, Universidade Nova de Lisboa, Portugal
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol118-concur2018/LIPIcs.CONCUR.2018.30/LIPIcs.CONCUR.2018.30.pdf
Session types
sharing
pi-calculus
bisimulation