Global types with internal delegation - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Theoretical Computer Science Année : 2020

Global types with internal delegation

Résumé

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.
Fichier principal
Vignette du fichier
cdgh19.pdf (305.56 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02419937 , version 1 (07-01-2020)

Identifiants

Citer

Ilaria Castellani, Mariangiola Dezani-Ciancaglini, Paola Giannini, Ross Horne. Global types with internal delegation. Theoretical Computer Science, 2020, 807, pp.26. ⟨10.1016/j.tcs.2019.09.027⟩. ⟨hal-02419937⟩
73 Consultations
138 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More