A universal session type for untyped asynchronous communication

Stephanie Balzer, Frank Pfenning, Bernardo Toninho

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publication29th International Conference on Concurrency Theory, CONCUR 2018
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Volume118
ISBN (Print)9783959770873
DOIs
Publication statusPublished - 1 Aug 2018
Event29th International Conference on Concurrency Theory, CONCUR 2018 - Beijing, China
Duration: 4 Sep 20187 Sep 2018

Conference

Conference29th International Conference on Concurrency Theory, CONCUR 2018
CountryChina
CityBeijing
Period4/09/187/09/18

Keywords

  • Bisimulation
  • Phrases session types
  • Sharing
  • Π-calculus

Fingerprint Dive into the research topics of 'A universal session type for untyped asynchronous communication'. Together they form a unique fingerprint.

  • Cite this

    Balzer, S., Pfenning, F., & Toninho, B. (2018). A universal session type for untyped asynchronous communication. In 29th International Conference on Concurrency Theory, CONCUR 2018 (Vol. 118). [30] Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.CONCUR.2018.30