A universal session type for untyped asynchronous communication

In the simply-typed λ-calculus we can recover the full range of expressiveness of the untyped λ-calculus solely by adding a single recursive type U = U → U. In contrast, in the session-typed π-calculus, recursion alone is insu cient to recover the untyped π-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 SILLS developed in prior work) are enough to embed the untyped asynchronous π-calculus via a universal shared session type US. We show that our encoding of the asynchronous π-calculus satisfies operational correspondence and preserves observable actions (i.e., processes are weakly bisimilar to their encoding). Moreover, we clarify the expressiveness of SILLS by developing an operationally correct encoding of SILLS in the asynchronous π-calculus.publishersversionpublishe