Skip to Main content Skip to Navigation
Journal articles

Reversible sessions with flexible choices

Abstract : We propose a calculus for concurrent reversible multiparty sessions, equipped with a flexible choice operator allowing for different sets of participants in each branch. This operator is inspired by the notion of connecting action recently introduced by Hu and Yoshida to describe protocols with optional participants. We argue that this choice operator allows for a natural description of typical communication protocols. Our calculus also supports a compact representation of the history of processes and types, which facilitates the definition of rollback. Moreover, it implements a fine-tuned strategy for backward computation. We present a session type system for the calculus and show that it enforces the expected properties of session fidelity, forward progress and backward progress.
Document type :
Journal articles
Complete list of metadata
Contributor : Ilaria Castellani <>
Submitted on : Thursday, December 19, 2019 - 11:07:17 PM
Last modification on : Monday, January 13, 2020 - 10:46:45 AM




Ilaria Castellani, Mariangiola Dezani-Ciancaglini, Paola Giannini. Reversible sessions with flexible choices. Acta Informatica, Springer Verlag, 2019, 56 (7-8), pp.553-583. ⟨10.1007/s00236-019-00332-y⟩. ⟨hal-02420508⟩



Record views