Publicação
A universal session type for untyped asynchronous communication
| dc.contributor.author | Balzer, Stephanie | |
| dc.contributor.author | Pfenning, Frank | |
| dc.contributor.author | Toninho, Bernardo | |
| dc.contributor.institution | DI - Departamento de Informática | |
| dc.date.accessioned | 2019-03-26T23:07:48Z | |
| dc.date.available | 2019-03-26T23:07:48Z | |
| dc.date.issued | 2018-08-01 | |
| dc.description | ||
| dc.description.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. | en |
| dc.description.version | publishersversion | |
| dc.description.version | published | |
| dc.format.extent | 677368 | |
| dc.identifier.doi | 10.4230/LIPIcs.CONCUR.2018.30 | |
| dc.identifier.isbn | 9783959770873 | |
| dc.identifier.other | PURE: 5933565 | |
| dc.identifier.other | PURE UUID: 4a25191d-400a-4a1b-aa2a-d06b638525fb | |
| dc.identifier.other | Scopus: 85053595048 | |
| dc.identifier.other | ORCID: /0000-0002-0746-7514/work/50464921 | |
| dc.identifier.uri | http://www.scopus.com/inward/record.url?scp=85053595048&partnerID=8YFLogxK | |
| dc.identifier.url | https://www.scopus.com/pages/publications/85053595048 | |
| dc.language.iso | eng | |
| dc.peerreviewed | yes | |
| dc.publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing | |
| dc.relation | info:eu-repo/grantAgreement/FCT/5876/147279/PT | |
| dc.subject | Bisimulation | |
| dc.subject | Phrases session types | |
| dc.subject | Sharing | |
| dc.subject | Π-calculus | |
| dc.subject | Software | |
| dc.title | A universal session type for untyped asynchronous communication | en |
| dc.type | conference object | |
| degois.publication.title | 29th International Conference on Concurrency Theory, CONCUR 2018 | |
| degois.publication.title | 29th International Conference on Concurrency Theory, CONCUR 2018 | |
| degois.publication.volume | 118 | |
| dspace.entity.type | Publication | |
| oaire.awardNumber | UID/CEC/04516/2013 | |
| oaire.awardURI | info:eu-repo/grantAgreement/FCT/5876/UID%2FCEC%2F04516%2F2013/PT | |
| oaire.fundingStream | 5876 | |
| project.funder.identifier | http://doi.org/10.13039/501100001871 | |
| project.funder.name | Fundação para a Ciência e a Tecnologia | |
| rcaap.rights | openAccess | |
| relation.isProjectOfPublication | 1f91d15d-5c38-4f20-87b3-0a1dfc82dcd9 | |
| relation.isProjectOfPublication.latestForDiscovery | 1f91d15d-5c38-4f20-87b3-0a1dfc82dcd9 |
Ficheiros
Principais
1 - 1 de 1
A carregar...
- Nome:
- LIPIcs_CONCUR_2018_30.pdf
- Tamanho:
- 661.49 KB
- Formato:
- Adobe Portable Document Format