On Global Types and Multi-Party Session
Global types are formal specifications that describe communication protocols in terms of their global interactions. We present a new, streamlined language of global types equipped with a trace-based semantics and whose features and restrictions are semantically justified. The multi-party sessions ob...
Main Authors: | , , |
---|---|
Format: | Article |
Language: | English |
Published: |
Logical Methods in Computer Science e.V.
2012-03-01
|
Series: | Logical Methods in Computer Science |
Subjects: | |
Online Access: | https://lmcs.episciences.org/773/pdf |
_version_ | 1797268705555513344 |
---|---|
author | Giuseppe Castagna Mariangiola Dezani-Ciancaglini Luca Padovani |
author_facet | Giuseppe Castagna Mariangiola Dezani-Ciancaglini Luca Padovani |
author_sort | Giuseppe Castagna |
collection | DOAJ |
description | Global types are formal specifications that describe communication protocols
in terms of their global interactions. We present a new, streamlined language
of global types equipped with a trace-based semantics and whose features and
restrictions are semantically justified. The multi-party sessions obtained
projecting our global types enjoy a liveness property in addition to the
traditional progress and are shown to be sound and complete with respect to the
set of traces of the originating global type. Our notion of completeness is
less demanding than the classical ones, allowing a multi-party session to leave
out redundant traces from an underspecified global type. In addition to the
technical content, we discuss some limitations of our language of global types
and provide an extensive comparison with related specification languages
adopted in different communities. |
first_indexed | 2024-04-25T01:36:44Z |
format | Article |
id | doaj.art-92e7b3034e424c90bee30037e53051c3 |
institution | Directory Open Access Journal |
issn | 1860-5974 |
language | English |
last_indexed | 2024-04-25T01:36:44Z |
publishDate | 2012-03-01 |
publisher | Logical Methods in Computer Science e.V. |
record_format | Article |
series | Logical Methods in Computer Science |
spelling | doaj.art-92e7b3034e424c90bee30037e53051c32024-03-08T09:27:54ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742012-03-01Volume 8, Issue 110.2168/LMCS-8(1:24)2012773On Global Types and Multi-Party SessionGiuseppe CastagnaMariangiola Dezani-CiancagliniLuca Padovanihttps://orcid.org/0000-0001-9097-1297Global types are formal specifications that describe communication protocols in terms of their global interactions. We present a new, streamlined language of global types equipped with a trace-based semantics and whose features and restrictions are semantically justified. The multi-party sessions obtained projecting our global types enjoy a liveness property in addition to the traditional progress and are shown to be sound and complete with respect to the set of traces of the originating global type. Our notion of completeness is less demanding than the classical ones, allowing a multi-party session to leave out redundant traces from an underspecified global type. In addition to the technical content, we discuss some limitations of our language of global types and provide an extensive comparison with related specification languages adopted in different communities.https://lmcs.episciences.org/773/pdfcomputer science - programming languagesf.1.2, f.3.3, h.3.5, h.5.3 |
spellingShingle | Giuseppe Castagna Mariangiola Dezani-Ciancaglini Luca Padovani On Global Types and Multi-Party Session Logical Methods in Computer Science computer science - programming languages f.1.2, f.3.3, h.3.5, h.5.3 |
title | On Global Types and Multi-Party Session |
title_full | On Global Types and Multi-Party Session |
title_fullStr | On Global Types and Multi-Party Session |
title_full_unstemmed | On Global Types and Multi-Party Session |
title_short | On Global Types and Multi-Party Session |
title_sort | on global types and multi party session |
topic | computer science - programming languages f.1.2, f.3.3, h.3.5, h.5.3 |
url | https://lmcs.episciences.org/773/pdf |
work_keys_str_mv | AT giuseppecastagna onglobaltypesandmultipartysession AT mariangioladezaniciancaglini onglobaltypesandmultipartysession AT lucapadovani onglobaltypesandmultipartysession |