ITU

On the boundary between decidability and undecidability of asynchronous session subtyping

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

Standard

On the boundary between decidability and undecidability of asynchronous session subtyping. / Bravetti, Mario; Carbone, Marco; Zavattaro, Gianluigi.

In: Theoretical Computer Science, Vol. 722, 2018, p. 19-51.

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

Harvard

APA

Vancouver

Author

Bibtex

@article{c14af606875b4a55a816fa99fae8c49d,
title = "On the boundary between decidability and undecidability of asynchronous session subtyping",
abstract = "Session types are behavioural types for guaranteeing that concurrent programs are free from basic communication errors. Recent work has shown that asynchronous session subtyping is undecidable. However, since session types have become popular in mainstream programming languages in which asynchronous communication is the norm rather than the exception, it is crucial to detect significant decidable subtyping relations. Previous work considered extremely restrictive fragments in which limitations were imposed to the size of communication buffer (at most 1) or to the possibility to express multiple choices (disallowing them completely in one of the compared types). In this work, for the first time, we show decidability of a fragment that does not impose any limitation on communication buffers and allows both the compared types to include multiple choices for either input or output, thus yielding a fragment which is more significant from an applicability viewpoint. In general, we study the boundary between decidability and undecidability by considering several fragments of subtyping. Notably, we show that subtyping remains undecidable even if restricted to not using output covariance and input contravariance.",
author = "Mario Bravetti and Marco Carbone and Gianluigi Zavattaro",
year = "2018",
doi = "10.1016/j.tcs.2018.02.010",
language = "English",
volume = "722",
pages = "19--51",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",

}

RIS

TY - JOUR

T1 - On the boundary between decidability and undecidability of asynchronous session subtyping

AU - Bravetti, Mario

AU - Carbone, Marco

AU - Zavattaro, Gianluigi

PY - 2018

Y1 - 2018

N2 - Session types are behavioural types for guaranteeing that concurrent programs are free from basic communication errors. Recent work has shown that asynchronous session subtyping is undecidable. However, since session types have become popular in mainstream programming languages in which asynchronous communication is the norm rather than the exception, it is crucial to detect significant decidable subtyping relations. Previous work considered extremely restrictive fragments in which limitations were imposed to the size of communication buffer (at most 1) or to the possibility to express multiple choices (disallowing them completely in one of the compared types). In this work, for the first time, we show decidability of a fragment that does not impose any limitation on communication buffers and allows both the compared types to include multiple choices for either input or output, thus yielding a fragment which is more significant from an applicability viewpoint. In general, we study the boundary between decidability and undecidability by considering several fragments of subtyping. Notably, we show that subtyping remains undecidable even if restricted to not using output covariance and input contravariance.

AB - Session types are behavioural types for guaranteeing that concurrent programs are free from basic communication errors. Recent work has shown that asynchronous session subtyping is undecidable. However, since session types have become popular in mainstream programming languages in which asynchronous communication is the norm rather than the exception, it is crucial to detect significant decidable subtyping relations. Previous work considered extremely restrictive fragments in which limitations were imposed to the size of communication buffer (at most 1) or to the possibility to express multiple choices (disallowing them completely in one of the compared types). In this work, for the first time, we show decidability of a fragment that does not impose any limitation on communication buffers and allows both the compared types to include multiple choices for either input or output, thus yielding a fragment which is more significant from an applicability viewpoint. In general, we study the boundary between decidability and undecidability by considering several fragments of subtyping. Notably, we show that subtyping remains undecidable even if restricted to not using output covariance and input contravariance.

U2 - 10.1016/j.tcs.2018.02.010

DO - 10.1016/j.tcs.2018.02.010

M3 - Journal article

VL - 722

SP - 19

EP - 51

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

ER -

ID: 83501417