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...

Full description

Bibliographic Details
Main Authors: Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, Luca Padovani
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