Multiparty sessions describe the interactions among multiple agents in a distributed environment and require essentially two steps: the specification of the communication protocols and the implementation of such protocols as processes. Multiparty session types address this methodology: global and session types provide the communication protocols, whereas the processes describe the behaviour of the peers involved in the sessions. Because of the close relationships between types and processes, some information, such as the names of senders and receivers, are replicated both in types and in processes. In multiparty conversations it is quite natural that participants with essentially the same role are implemented by processes that follow the same pattern, differing only in the senders and receivers of communication actions. In order to allow for a lighter and less rigid development of processes, we propose a translation tool which allows one to write processes in a simplified syntax, called partial syntax, where the names of senders/receivers for input/output operations are omitted. By adding the missing information, partial processes can be automatically translated in complete process, for which an operational semantics is defined. The partial syntax, in particular, allows one to use the same process template to implement similar participants. In this paper we present a translation and type checking algorithm from partial to complete processes, which, if successful, also assures that the target processes are well typed. The algorithm is synthesised from a rule-based description of the translation in natural semantics and it is proved sound and complete with respect to the translation rules.

Partial and Complete Processes in Multiparty Sessions

COPPO, Mario;DEZANI, Mariangiola;MARGARIA, Ines Maria;ZACCHI, Maddalena
2015-01-01

Abstract

Multiparty sessions describe the interactions among multiple agents in a distributed environment and require essentially two steps: the specification of the communication protocols and the implementation of such protocols as processes. Multiparty session types address this methodology: global and session types provide the communication protocols, whereas the processes describe the behaviour of the peers involved in the sessions. Because of the close relationships between types and processes, some information, such as the names of senders and receivers, are replicated both in types and in processes. In multiparty conversations it is quite natural that participants with essentially the same role are implemented by processes that follow the same pattern, differing only in the senders and receivers of communication actions. In order to allow for a lighter and less rigid development of processes, we propose a translation tool which allows one to write processes in a simplified syntax, called partial syntax, where the names of senders/receivers for input/output operations are omitted. By adding the missing information, partial processes can be automatically translated in complete process, for which an operational semantics is defined. The partial syntax, in particular, allows one to use the same process template to implement similar participants. In this paper we present a translation and type checking algorithm from partial to complete processes, which, if successful, also assures that the target processes are well typed. The algorithm is synthesised from a rule-based description of the translation in natural semantics and it is proved sound and complete with respect to the translation rules.
Italian Conference on Theoretical Computer Science (ICTCS)
Firenze
9-11 September 2015
322
135
151
http://www.di.unito.it/~dezani/papers/cdmz15b.pdf
sistemi concorrenti, tipi sessione, inferenza automatica
Coppo, Mario; Dezani, Mariangiola; Margaria, Ines; Zacchi, Maddalena
File in questo prodotto:
File Dimensione Formato  
1-s2.0-S1571066116300184-main.pdf

Accesso aperto

Descrizione: Articolo completo
Tipo di file: PDF EDITORIALE
Dimensione 302.63 kB
Formato Adobe PDF
302.63 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/1577947
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
social impact