Global types with internal delegation

Tools

Castellani, Ilaria and Dezani-Ciancaglini, Mariangiola and Giannini, Paola and Horne, Ross (2020) Global types with internal delegation. Theoretical Computer Science, 807. 128 - 153. ISSN 0304-3975 (https://doi.org/10.1016/j.tcs.2019.09.027)

[thumbnail of Castellani-etal-TCS2020-Global-types-internal-delegation]
Preview
 Text. Filename: Castellani_etal_TCS2020_Global_types_internal_delegation.pdf
Accepted Author Manuscript
License: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 logo
Download (471kB)| Preview

Abstract

This paper investigates a new form of delegation for multiparty session calculi. Usually, delegation allows a session participant to appoint a participant in another session to act on her behalf. This means that delegation is inherently an inter-session mechanism, which requires session interleaving. Hence delegation falls outside the descriptive power of global types, which specify single sessions. As a consequence, properties such as deadlock-freedom or lock-freedom are difficult to ensure in the presence of delegation. Here we adopt a different view of delegation, by allowing participants to delegate tasks to each other within the same multiparty session. This way, delegation occurs within a single session (internal delegation) and may be captured by its global type. To increase flexibility in the use of delegation, our calculus uses connecting communications, which allow optional participants in the branches of choices. By these means, we are able to express conditional delegation. We present a session type system based on global types with internal delegation, and show that it ensures the usual safety properties of multiparty sessions, together with a progress property.

ORCID iDs

Castellani, Ilaria, Dezani-Ciancaglini, Mariangiola, Giannini, Paola and Horne, Ross ORCID logoORCID: https://orcid.org/0000-0003-0162-1901;
  • Item type:Article
    ID code:86943
    Dates:
    Date
    Event
    6 February 2020
    Published
    23 September 2019
    Published Online
    17 September 2019
    Accepted
    15 September 2018
    Submitted
    Notes:In memory of Maurice Nivat, a founding father of Theoretical Computer Science - Part II Ilaria Castellani, Mariangiola Dezani-Ciancaglini, Paola Giannini, Ross Horne, Global types with internal delegation, Theoretical Computer Science, Volume 807, 2020, Pages 128-153, https://doi.org/10.1016/j.tcs.2019.09.027
    Subjects:Science > Mathematics > Electronic computers. Computer science
    Department:Faculty of Science > Computer and Information Sciences
    Depositing user: Pure Administrator
    Date deposited:12 Oct 2023 10:44
    Last modified:11 Nov 2024 14:04
    Related URLs:
    URI:https://strathprints.strath.ac.uk/id/eprint/86943
CORE (COnnecting REpositories)