A multiparty session formalises a set of concurrent communicating participants. The possibility for a participant to delegate some interactions to another participant is crucial for the expressivity of multiparty sessions. We propose the first type system for multiparty sessions with delegation where some communications between participants can be ignored. This allows us to type some sessions with global types representing interesting protocols, which have no type in the standard type systems. Our type system enjoys Subject Reduction, Session Fidelity and partial Lock-freedom. The last property ensures the absence of locks for participants with non-ignored communications. A sound and complete type inference algorithm is also discussed.

Partially typed multiparty sessions with internal delegation

Bono, Viviana;Dezani-Ciancaglini, Mariangiola
2025-01-01

Abstract

A multiparty session formalises a set of concurrent communicating participants. The possibility for a participant to delegate some interactions to another participant is crucial for the expressivity of multiparty sessions. We propose the first type system for multiparty sessions with delegation where some communications between participants can be ignored. This allows us to type some sessions with global types representing interesting protocols, which have no type in the standard type systems. Our type system enjoys Subject Reduction, Session Fidelity and partial Lock-freedom. The last property ensures the absence of locks for participants with non-ignored communications. A sound and complete type inference algorithm is also discussed.
2025
142
101018
101018
https://www.sciencedirect.com/science/article/pii/S2352220824000725?via=ihub
Communication-based programming; Delegation; Multiparty session types; Process calculi
Barbanera, Franco; Bono, Viviana; Dezani-Ciancaglini, Mariangiola
File in questo prodotto:
File Dimensione Formato  
1-s2.0-S2352220824000725-main.pdf

Accesso aperto

Tipo di file: PDF EDITORIALE
Dimensione 822.99 kB
Formato Adobe PDF
822.99 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/2067157
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 1
social impact