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

Fingerprint

Semantics
Communication

Keywords

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

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
Balzer, Stephanie ; Pfenning, Frank ; Toninho, Bernardo. / A universal session type for untyped asynchronous communication. 29th International Conference on Concurrency Theory, CONCUR 2018. Vol. 118 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2018.
@inproceedings{4a25191d400a4a1baa2ad06b638525fb,
title = "A universal session type for untyped asynchronous communication",
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.",
keywords = "Bisimulation, Phrases session types, Sharing, Π-calculus",
author = "Stephanie Balzer and Frank Pfenning and Bernardo Toninho",
note = "info:eu-repo/grantAgreement/FCT/5876/147279/PT#",
year = "2018",
month = "8",
day = "1",
doi = "10.4230/LIPIcs.CONCUR.2018.30",
language = "English",
isbn = "9783959770873",
volume = "118",
booktitle = "29th International Conference on Concurrency Theory, CONCUR 2018",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",

}

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, 29th International Conference on Concurrency Theory, CONCUR 2018, Beijing, China, 4/09/18. https://doi.org/10.4230/LIPIcs.CONCUR.2018.30

A universal session type for untyped asynchronous communication. / Balzer, Stephanie; Pfenning, Frank; Toninho, Bernardo.

29th International Conference on Concurrency Theory, CONCUR 2018. Vol. 118 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2018. 30.

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

TY - GEN

T1 - A universal session type for untyped asynchronous communication

AU - Balzer, Stephanie

AU - Pfenning, Frank

AU - Toninho, Bernardo

N1 - info:eu-repo/grantAgreement/FCT/5876/147279/PT#

PY - 2018/8/1

Y1 - 2018/8/1

N2 - 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.

AB - 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.

KW - Bisimulation

KW - Phrases session types

KW - Sharing

KW - Π-calculus

UR - http://www.scopus.com/inward/record.url?scp=85053595048&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.CONCUR.2018.30

DO - 10.4230/LIPIcs.CONCUR.2018.30

M3 - Conference contribution

SN - 9783959770873

VL - 118

BT - 29th International Conference on Concurrency Theory, CONCUR 2018

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

ER -

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