# A simple view of multiparty session types

Ilaria Castellani

► To cite this version:

Ilaria Castellani. A simple view of multiparty session types. PPDP 2024 - 26th International Symposium on Principles and Practice of Declarative Programming, Sep 2024, Milano Italy, Italy. pp.1 - 3, 10.1145/3678232.3678252. hal-04895577

HAL Id: hal-04895577

https://inria.hal.science/hal-04895577v1

Submitted on 18 Jan 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# A simple view of multiparty session types

Ilaria Castellani

INRIA, Université Côte d'Azur

Sophia Antipolis, France

ilaria.castellani@inria.fr

## CCS CONCEPTS

* Theory of computation → Process calculi; Type theory.

## KEYWORDS

Session types, pi-calculus, multiparty sessions

**ACM Reference Format:**

Ilaria Castellani. 2024. A simple view of multiparty session types. In *26th International Symposium on Principles and Practice of Declarative Programming (PPDP 2024), September 09–11, 2024, Milano, Italy*. ACM, New York, NY, USA, 3 pages. https://doi.org/10.1145/3678232.3678252

Session types are an abstract description of sessions, which are structured interactions involving two or more participants. They specify the sequence of messages exchanged by participants as well as their functionality (sender, receiver and type of carried data). Session types belong to the family of behavioural types [14], which describe an interaction step by step while abstracting from the values of data and from internal computations. They may be viewed as the analogue, for concurrency and distribution, of data types for sequential computation. Originally conceived as a static analysis technique for a variant of the π-calculus [11, 21], session types have been progressively embedded into a range of functional, concurrent, and object-oriented programming languages [1].

Session types were first used to describe binary sessions [10, 11, 21, 23], which may typically be regarded as client-server interactions. What is required for a binary session to proceed smoothly is that the two participants have compatible behaviours, i.e. matching expectations. Formally, this is expressed by requiring that the types specifying the participants' behaviours be dual to each other: if one participant is ready to receive a value of type T the other sends a value of type T, and vice versa. Hence, the type of a binary session is completely determined by the type of any of its two participants. Besides the send and receive operators, session calculi also feature two choice operators for process interaction: an external choice operator offering a range of options (typically appearing in the server), and an internal choice operator used to select one option in a given range (typically appearing in the client). These operators reflect common patterns occurring in communication protocols and web services.

Subsequently, session types have been extended to multiparty sessions [12, 13], where several participants interact with each other. A multiparty session is an interaction among peers. Hence, a priori

there is no need to distinguish one of the participants as representing the server. Rather, each participant may act in turn as a server or as a client for other participants at different stages of the interaction. As expected, ensuring session correctness is more difficult for multiparty sessions than for binary sessions. In particular, the requirement of duality does not generalise easily to multiparty sessions: in order for a multiparty session to execute successfully, it is not enough that any two participants have matching expectations with respect to each other. In other words, the multiparty compatibility of a set of behaviours does not amount to their pairwise compatibility. To illustrate this point, let us consider a session with three participants, each playing the role of a philosopher in the classical *dining philosophers* example. The three philosophers are sitting in a circle and each of them waits for a message from its left neighbour before sending a message to its right neighbour. Clearly, any two participants have matching mutual expectations, but nevertheless the session is stuck, due to a circular dependency that can only be detected at the global level, by considering all the participants' behaviours at once.

Several definitions of multiparty compatibility have been put forward. A popular approach, following the original proposal of [12, 13], consists in adopting two kinds of types for describing multiparty sessions: a *global type* that describes the whole session protocol, and *local types* that describe the individual contributions of the participants to the protocol. Then, the key requirement to achieve session correctness is that the local types of the processes implementing the participants be obtained as projections from the same global type.

The session correctness properties ensured by session types are communication safety, meaning that there is no mismatch in the direction and type of exchanged messages, and protocol conformance, also called session fidelity, meaning that session communications follow the order prescribed by the protocol. When the session is run in isolation, or in parallel with sessions with disjoint participants, session types also ensure deadlock-freedom [13], i.e. the pursuit of the session until all participants are terminated. For instance, the deadlocked 3-philosopher session discussed above will be ruled out, since there is no global type that projects down to the local types of its participants. However, deadlock-freedom cannot be guaranteed anymore when different sessions with common participants are run in parallel, since the order in which participants contribute to different sessions cannot be captured by global types, each of which describes a single session. To ensure deadlock-freedom in the presence of session interleaving, the session type system needs to be complemented with a static analysis that tracks the order in which different session channels are used by processes. Such analyses are often quite sophisticated [15, 16, 18].

For this reason, several recent studies on multiparty session types have departed from the original proposal of [12, 13], which

<footnote>Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the owner/author(s).

PPDP 2024, September 09–11, 2024, Milano, Italy

© 2024 Copyright held by the owner/author(s).

ACM ISBN 979-8-4007-0969-2/24/09

https://doi.org/10.1145/3678232.3678252</footnote>
allowed session interleaving, by focussing on the "single session scenario" where sessions are run in isolation. In such a scenario, one can do away with the session creation primitive. More importantly, one can omit session channels altogether, as suggested in [9], by replacing them with explicit participants. Then, a multiparty session may be simply described as a network of sequential processes, each pertaining to a distinct participant. Following [8], we shall refer to such multiparty sessions without channels as *simple multiparty sessions*. This simplification allows us to focus on the specific features of multiparty sessions, such as the various options for defining the projection operation and related issues concerning the choice operator. Additionally, it makes it easier to address the well-formedness conditions required for global types to ensure the mentioned safety properties and to rule out starvation, thereby ensuring the liveness property of *lock-freedom*, also called *progress*.

By giving up session interleaving and session channels, it may seem that one drastically cuts down the expressive power of session calculi. In particular, the classical mechanism of *delegation* [11], by which a session participant may appoint a participant in another session to act on its behalf, requires session interleaving and crucially relies on the ability of $\pi$-calculus processes to send channels over channels. However, being inherently an inter-session mechanism, this kind of delegation falls outside the descriptive power of global types, which can only specify single sessions. As a consequence, properties such as deadlock-freedom or lock-freedom are difficult to ensure in the presence of delegation. To overcome this problem, a new form of delegation was proposed in [4] for simple multiparty sessions, whereby participants are allowed to delegate tasks to each other within the *same* multiparty session. This kind of delegation, called *internal delegation*, occurs within a single session and thus may be captured by its global type. The associated session type system ensures the usual safety properties of multiparty sessions, together with a progress property. Hence, by switching from external to internal delegation, the apparent loss of expressive power caused by the omission of channels turns into a gain of semantic guarantees.

A further simplification in the treatment of multiparty session types has been proposed in the recent work [6]. The idea here is to get rid of local types for processes and of the projection operation, by using typing rules that directly assign global types to sessions. The key observation is that, in order for the type system to enjoy both type preservation and session fidelity, the LTS of a session must be bisimilar to the LTS of any of its global types. Hence, for a global type *G* to type a session *N*, it is enough to require that all the derivatives $N'$ of *N* be typable by corresponding derivatives $G'$ of *G*.

My talk will briefly recount the genesis and evolution of session types since their introduction in the mid-nineties. It will then focus on some recent results on simple multiparty session types, including their connection with the semantic model of Event Structures [24]. Specifically, the use of Event Structures as a denotational model for both multiparty sessions and their global types was investigated in [2] and [3], assuming respectively synchronous and asynchronous communication. The subsequent work [5] highlights the interest of such a denotational model by proposing semantic counterparts for the well-formedness conditions of global types.

The talk will conclude with a short review on the connection between multiparty session types and other concurrency models such as communicating automata [7], graphical choreographies [17, 22] and message sequence charts [19, 20].

## REFERENCES

[1] Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Deniélou, Simon J. Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T. Vasconcelos, and Nobuko Yoshida. 2016. Behavioral types in programming languages. *Foundations and Trends in Programming Languages* 3, 2-3 (2016), 95-230. https://doi.org/10.1561/2500000031

[2] Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Paola Giannini. 2023. Event structure semantics for multiparty sessions. *Journal of Logic and Algebraic Methods in Programming* 131 (2023), 100844. https://doi.org/10.1016/j.jlamp.2022.100844

[3] Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Paola Giannini. 2024. Global types and event structure semantics for asynchronous multiparty sessions. *Fundamenta Informaticae* 192, 1 (2024), 1-75. https://doi.org/10.48550/arXiv.2102.00865

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

[5] Ilaria Castellani and Paola Giannini. 2024. Towards a semantic characterisation of global type well-formedness. In *PLACES (EPTCS, Vol. 401)*, Diana Costa and Raymond Hu (Eds.). Open Publishing Association, Waterloo, 11-21. https://doi.org/10.4204/EPTCS.401.2

[6] Francesco Dagnino, Paola Giannini, and Mariangiola Dezani-Ciancaglini. 2023. Deconfined global types for asynchronous sessions. *Logical Methods in Computer Science* 19, 1 (2023), 1-41. https://doi.org/10.46298/lmcs-19(1:3)2023

[7] Pierre-Malo Deniélou and Nobuko Yoshida. 2012. Multiparty session types meet communicating automata. In *ESOP (LNCS, Vol. 7211)*, Helmut Seidl (Ed.). Springer, Heidelberg, 194-213. https://doi.org/10.1007/978-3-642-28869-2_10

[8] Mariangiola Dezani-Ciancaglini. 2024. Simple multiparty sessions. Invited talk, PLACES, http://www.di.unito.it/~dezani/papers/places.pdf.

[9] Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Svetlana Jaksic, Jovanka Pantic, and Nobuko Yoshida. 2015. Precise subtyping for synchronous multiparty sessions. In *PLACES (EPTCS, Vol. 203)*, Simon Gay and Jade Alglave (Eds.). Open Publishing Association, Waterloo, 29-44. https://doi.org/10.4204/EPTCS.203.3

[10] Simon Gay and Malcolm Hole. 2005. Subtyping for session types in the pi calculus. *Acta Informatica* 42, 2/3 (2005), 191-225. https://doi.org/10.1007/s00236-005-0177-z

[11] Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. 1998. Language primitives and type discipline for structured communication-based programming. In *ESOP (LNCS, Vol. 1381)*, Chris Hankin (Ed.). Springer, Heidelberg, 122-138. https://doi.org/10.1007/BFb0053567

[12] Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2008. Multiparty asynchronous session types. In *POPL*, George C. Necula and Philip Wadler (Eds.). ACM Press, New York, 273-284. https://doi.org/10.1145/1328897.1328472

[13] Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2016. Multiparty asynchronous session types. *Journal of ACM* 63, 1 (2016), 9:1-9:67. https://doi.org/10.1145/2827695

[14] Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Luis Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, Hugo Torres Vieira, and Gianluigi Zavattaro. 2016. Foundations of session types and behavioural contracts. *Comput. Surveys* 49, 1, Article 3 (2016), 36 pages. https://doi.org/10.1145/2873052

[15] Naoki Kobayashi. 2002. A type system for lock-free processes. *Information and Computation* 177, 2 (2002), 122-159. https://doi.org/10.1016/S0890-5401(02)93171-8

[16] Naoki Kobayashi. 2006. A new type system for deadlock-free processes. In *CONCUR (LNCS, Vol. 4137)*, Christel Baier and Holger Hermanns (Eds.). Springer, Heidelberg, 233-247. https://doi.org/10.1007/11817949_16

[17] Julien Lange, Emilio Tuosto, and Nobuko Yoshida. 2015. From communicating machines to graphical choreographies. In *POPL*, Sriram K. Rajamani and David Walker (Eds.). ACM Press, New York, 221-232. https://doi.org/10.1145/2676726.2676964

[18] Luca Padovani. 2014. Deadlock and lock freedom in the linear $\pi$-calculus. In *CSL-LICS*, Thomas A. Henzinger and Dale Miller (Eds.). ACM, New York, 721-7210. https://doi.org/10.1145/2603088.2603116

[19] Felix Stutz. 2023. Asynchronous multiparty session type implementability is decidable - Lessons learned from message sequence charts. In *ECOOP (LIPICS, Vol. 263)*, Karim Ali and Guido Salvaneschi (Eds.). Leibniz-Zentrum für Informatik, Schloss Dagstuhl, 32:1-32:31. https://doi.org/10.4230/LIPICS.ECOOP.2023.32
[20] Felix Stutz and Damien Zufferey. 2022. Comparing channel restrictions of communicating state machines, high-level message sequence charts, and multiparty session types. In *GandALF (EPTCS, Vol. 370)*, Pierre Ganty and Dario Della Monica (Eds.). Open Publishing Association, Waterloo, 194–212. https://doi.org/10.4204/EPTCS.370.13

[21] Kaku Takeuchi, Kohei Honda, and Makoto Kubo. 1994. An interaction-based language and its typing system. In *PARLE (LNCS, Vol. 817)*, Chris Hankin (Ed.). Springer, Heidelberg, 122–138. https://doi.org/10.1007/3-540-58184-7_118

[22] Emilio Tuosto and Roberto Guanciale. 2018. Semantics of global view of choreographies. *Journal of Logic and Algebraic Methods in Programming* 95 (2018), 17–40. https://doi.org/10.1016/j.jlamp.2017.11.002

[23] Vasco T. Vasconcelos. 2012. Fundamentals of session types. *Information and Computation* 217 (2012), 52–70. https://doi.org/10.1016/j.ic.2012.05.002

[24] G. Winskel. 1986. Event structures. In *Petri nets: central models and their properties; advances in Petri nets (LNCS, 255)*, W. Brauer (Ed.). Springer, Heidelberg, 325–392. https://doi.org/10.1007/3-540-17906-2_31