View in EDS

On the boundary between decidability and undecidability of asynchronous session subtyping.

Saved in:
Bibliographic Details
Title: On the boundary between decidability and undecidability of asynchronous session subtyping.
Authors: Bravetti, Mario1 mario.bravetti@unibo.it, Carbone, Marco2, Zavattaro, Gianluigi1
Source: Theoretical Computer Science. Apr2018, Vol. 722, p19-51. 33p.
Subjects: Asynchronous transfer mode, Programming languages, Buffer storage (Computer science), Decidability (Mathematical logic), Mathematical models
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. [ABSTRACT FROM AUTHOR]
Copyright of Theoretical Computer Science is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 128391533
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: On the boundary between decidability and undecidability of asynchronous session subtyping.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Bravetti%2C+Mario%22">Bravetti, Mario</searchLink><relatesTo>1</relatesTo><i> mario.bravetti@unibo.it</i><br /><searchLink fieldCode="AR" term="%22Carbone%2C+Marco%22">Carbone, Marco</searchLink><relatesTo>2</relatesTo><br /><searchLink fieldCode="AR" term="%22Zavattaro%2C+Gianluigi%22">Zavattaro, Gianluigi</searchLink><relatesTo>1</relatesTo>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Theoretical+Computer+Science%22">Theoretical Computer Science</searchLink>. Apr2018, Vol. 722, p19-51. 33p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Asynchronous+transfer+mode%22">Asynchronous transfer mode</searchLink><br /><searchLink fieldCode="DE" term="%22Programming+languages%22">Programming languages</searchLink><br /><searchLink fieldCode="DE" term="%22Buffer+storage+%28Computer+science%29%22">Buffer storage (Computer science)</searchLink><br /><searchLink fieldCode="DE" term="%22Decidability+%28Mathematical+logic%29%22">Decidability (Mathematical logic)</searchLink><br /><searchLink fieldCode="DE" term="%22Mathematical+models%22">Mathematical models</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: 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. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Theoretical Computer Science is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=128391533
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1016/j.tcs.2018.02.010
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 33
        StartPage: 19
    Subjects:
      – SubjectFull: Asynchronous transfer mode
        Type: general
      – SubjectFull: Programming languages
        Type: general
      – SubjectFull: Buffer storage (Computer science)
        Type: general
      – SubjectFull: Decidability (Mathematical logic)
        Type: general
      – SubjectFull: Mathematical models
        Type: general
    Titles:
      – TitleFull: On the boundary between decidability and undecidability of asynchronous session subtyping.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Bravetti, Mario
      – PersonEntity:
          Name:
            NameFull: Carbone, Marco
      – PersonEntity:
          Name:
            NameFull: Zavattaro, Gianluigi
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 25
              M: 04
              Text: Apr2018
              Type: published
              Y: 2018
          Identifiers:
            – Type: issn-print
              Value: 03043975
          Numbering:
            – Type: volume
              Value: 722
          Titles:
            – TitleFull: Theoretical Computer Science
              Type: main
ResultId 1