Typing Liveness in Multiparty Communicating Systems

Session type systems are an effective tool to prove that communicating programs do not go wrong, ensuring that the participants of a session follow the protocols described by the types. In previous work, we have introduced a typing discipline for the analysis of progress in binary sessions. In this paper, we generalize the approach to multiparty sessions following the conversation type discipline, while strengthening progress to liveness. Conversation types allow to discipline interaction in systems where a possibly unanticipated number of multiple participants interact using a single medium of communication. We combine the usual session-like fidelity analysis with the liveness analysis and devise an original treatment of recursive types allowing us to address challenging configurations that are out of the reach of existing approaches.

Data and Resources

Additional Info

Field Value
Source https://inria.hal.science/hal-00960879
Author Padovani, Luca, Vasconcelos, Vasco T., Vieira, Hugo Torres
Maintainer CCSD
Last Updated May 6, 2026, 00:08 (UTC)
Created May 6, 2026, 00:08 (UTC)
Identifier hal-00960879
Language en
Rights https://about.hal.science/hal-authorisation-v1/
contributor Dipartimento di Informatica [Torino] ; Università degli studi di Torino = University of Turin (UNITO)
creator Padovani, Luca
date 2014-03-18T00:00:00
harvest_object_id 6962056e-e4e1-4cae-9824-75850ce7538e
harvest_source_id 3374d638-d20b-4672-ba96-a23232d55657
harvest_source_title test moissonnage SELUNE
metadata_modified 2025-12-18T00:00:00
set_spec type:UNDEFINED