Log in
Enquire now
‌

Comprehensive Multiparty Session Types

OverviewStructured DataIssuesContributors

Contents

Paper abstractTimelineTable: Further ResourcesReferences
Is a
‌
Academic paper
1

Academic Paper attributes

arXiv ID
1902.005441
arXiv Classification
Computer science
Computer science
1
Publication URL
arxiv.org/pdf/1902.00544v11
Publisher
ArXiv
ArXiv
1
DOI
doi.org/10.48550/ar...02.005441
Paid/Free
Free1
Academic Discipline
Computer science
Computer science
1
Programming language
Programming language
1
Submission Date
February 1, 2019
1
Author Names
Elton Domnori1
Patrick Eugster1
Mira Mezini1
Andi Bejleri1
Malte Viering1
Paper abstract

Multiparty session types (MST) are a well-established type theory that describes the interactive structure of a fixed number of components from a global point of view and type-checks the components through projection of the global type onto the participants of the session. They guarantee communicationsafety for a language of multiparty sessions (LMS), i.e., distributed, parallel components can exchange values without deadlocking and unexpected message types. Several variants of MST and LMS have been proposed to study key features of distributed and parallel programming. We observe that the population of the considered variants follows from only one ancestor, i.e., the original LMS/MST, and there are overlapping traits between features of the considered variants and the original. These hamper evolution of session types and languages and their adoption in practice. This paper addresses the following question: What are the essential features for MST and LMS, and how can these be modelled with simple constructs? To the best of our knowledge, this is the first time this question has been addressed. We performed a systematic analysis of the features and the constructs in MST, LMS, and the considered variants to identify the essential features. The variants are among the most influential (according to Google Scholar) and well-established systems that cover a wide set of areas in distributed, parallel programming. We used classical techniques of formal models such as BNF, structural congruence, small step operational semantics and typing judgments to build our language and type system. Lastly, the coherence of operational semantics and type system is proven by induction. This paper proposes a set of essential features, a language of structured interactions and a type theory of comprehensive multiparty session types, including global types and type system. The analysis removes overlapping features and captures the shared traits, thereby introducing the essential features. The constructs of the language are simple and fundamental, based on the lambda and pi calculi. Analogously, our global types reflect what is omitted and introduced in the language. Our system covers all the features of the original and variants, with a better ratio of the number of language and type constructs over the number of covered features. The features of the original, variants, and our system along with the number of constructs in the respective language and global types to model them are presented through a table. The syntax, operational semantics, meta-theory and type system of our system are given. We modelled all the motivating examples of the variants in our model, describing the reduction and typing steps. The work discusses how new features, in particular the non-essential ones (formerly excluded) and advanced ones can be either modelled atop the essential ones or added with minimal efforts, i.e. without modifying the existing ones. The fundamental properties of typed processes such as subject reduction, communication safety, and progress are established.

Timeline

No Timeline data yet.

Further Resources

Title
Author
Link
Type
Date
No Further Resources data yet.

References

Find more entities like Comprehensive Multiparty Session Types

Use the Golden Query Tool to find similar entities by any field in the Knowledge Graph, including industry, location, and more.
Open Query Tool
Access by API
Golden Query Tool
Golden logo

Company

  • Home
  • Press & Media
  • Blog
  • Careers
  • WE'RE HIRING

Products

  • Knowledge Graph
  • Query Tool
  • Data Requests
  • Knowledge Storage
  • API
  • Pricing
  • Enterprise
  • ChatGPT Plugin

Legal

  • Terms of Service
  • Enterprise Terms of Service
  • Privacy Policy

Help

  • Help center
  • API Documentation
  • Contact Us
By using this site, you agree to our Terms of Service.