Acta Informatica

, Volume 56, Issue 7–8, pp 553–583 | Cite as

Reversible sessions with flexible choices

  • Ilaria Castellani
  • Mariangiola Dezani-Ciancaglini
  • Paola GianniniEmail author
Original Article


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.



We would like to thank the anonymous referees for their helpful comments.


  1. 1.
    Barbanera, F., de’ Liguoro, U.: Sub-behaviour relations for session-based client/server systems. Math. Struct. Comput. Sci. 25(6), 1339–1381 (2015)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Barbanera, F., Dezani-Ciancaglini, M., de’Liguoro, U.: Reversible client/server interactions. Form. Asp. Comput. 28(4), 697–722 (2016)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Barbanera, F., Dezani-Ciancaglini, M., Lanese, I., de’ Liguoro, U.: Retractable contracts. In: PLACES, volume 203 of EPTCS, pp. 61–72 (2016)CrossRefGoogle Scholar
  4. 4.
    Bernardi, G., Hennessy, M.: Modelling session types using contracts. Math. Struct. Comput. Sci. 26(3), 510–560 (2016)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Boudol, G., Castellani, I.: Permutation of transitions: an event structure semantics for CCS and SCCS. In: REX School, volume 354 of LNCS, pp. 411–427. Springer (1988)Google Scholar
  6. 6.
    Boudol, G., Castellani, I.: Flow models of distributed computations: three equivalent semantics for CCS. Inf. Comput. 114(2), 247–314 (1994)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Caires, L., Vieira, H.T.: Analysis of service oriented software systems with the conversation calculus. In: FACS, volume 6921 of LNCS, pp. 6–33. Springer (2010)Google Scholar
  8. 8.
    Castellani, I., Dezani-Ciancaglini, M., Giannini, P.: Concurrent reversible sessions. In: CONCUR, volume 85 of LIPIcs, pp. 30:1–30:17. Schloss Dagstuhl (2017)Google Scholar
  9. 9.
    Cristescu, I., Krivine, J., Varacca, D.: Rigid families for the reversible \(\pi \)-calculus. In: RC, volume 9720 of LNCS, pp. 3–19. Springer (2016)Google Scholar
  10. 10.
    Danos, V., Krivine, J.: Reversible communicating systems. In: CONCUR, volume 3170 of LNCS, pp. 292–307. Springer (2004)Google Scholar
  11. 11.
    de Vries, E., Koutavas, V., Hennessy, M.: Communicating transactions—(extended abstract). In: CONCUR, volume 6269 of LNCS, pp. 569–583. Springer (2010)Google Scholar
  12. 12.
    de Vries, E., Koutavas, V., Hennessy, M.: Liveness of communicating transactions—(extended abstract). In: APLAS, volume 6461 of LNCS, pp. 392–407. Springer (2010)Google Scholar
  13. 13.
    Deniélou, P.-M., Yoshida, N.: Dynamic multirole session types. In: POPL, pp. 435–446. ACM Press (2011)Google Scholar
  14. 14.
    Dezani-Ciancaglini, M., Giannini, P.: Reversible multiparty sessions with checkpoints. In: EXPRESS/SOS, volume 222 of EPTCS, pp. 60–74 (2016)MathSciNetCrossRefGoogle Scholar
  15. 15.
    Giachino, E., Sackman, M., Drossopoulou, S., Eisenbach, S.: Softly safely spoken: Role playing for session types. In: PLACES (2009)Google Scholar
  16. 16.
    Graversen, E., Phillips, I., Yoshida, N.: Towards a categorical representation of reversible event structures. In: PLACES, volume 246 of EPTCS, pp. 49–60 (2017)MathSciNetCrossRefGoogle Scholar
  17. 17.
    Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type disciplines for structured communication-based programming. In: ESOP, volume 1381 of LNCS, pp. 22–138. Springer (1998)Google Scholar
  18. 18.
    Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL, pp. 273–284. ACM Press (2008)Google Scholar
  19. 19.
    Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. J. ACM 63(1), 9 (2016)MathSciNetCrossRefGoogle Scholar
  20. 20.
    Hu, R., Yoshida, N.: Explicit connection actions in multiparty session types. In: Fundamental Approaches to Software Engineering, volume 10202 of LNCS, pp. 116–133. Springer (2017)Google Scholar
  21. 21.
    Koutavas, V., Spaccasassi, C., Hennessy, M.: Bisimulations for communicating transactions—(extended abstract). In: FOSSACS, volume 8412 of LNCS, pp. 320–334. Springer (2014)Google Scholar
  22. 22.
    Lanese, I., Mezzina, C.A., Schmitt, A., Stefani, J.-B.: Controlling reversibility in higher-order pi. In: CONCUR, volume 6901 of LNCS, pp. 297–311. Springer (2011)Google Scholar
  23. 23.
    Lanese, I., Mezzina, C.A., Stefani, J.-B.: Reversing higher-order pi. In: CONCUR, volume 6269 of LNCS, pp. 478–493. Springer (2010)Google Scholar
  24. 24.
    Mezzina, C.A., Pérez, J.A.: Reversible semantics in session-based concurrency. In: ICTCS, volume 1720 of CEUR, pp. 221–226 (2016). CEUR-WS.orgGoogle Scholar
  25. 25.
    Mezzina, C.A., Pérez, J.A.: Reversible sessions using monitors. In: PLACES, volume 211 of EPTCS, pp. 56–64 (2016)CrossRefGoogle Scholar
  26. 26.
    Mezzina, C.A., Pérez, J.A.: Causally consistent reversible choreographies: a monitors-as-memories approach. In: PPDP, pp. 127–138. ACM Press (2017)Google Scholar
  27. 27.
    Mezzina, C.A., Tuosto, E.: Choreographies for automatic recovery (2017). CoRR, arXiv:1705.09525
  28. 28.
    Neykova, R., Yoshida, N.: Let it recover: multiparty protocol-induced recovery. In: CC, pp. 98–108. ACM Press (2017)Google Scholar
  29. 29.
    Padovani, L.: Type reconstruction for the linear \(\pi \)-calculus with composite regular types. Log. Methods Comput. Sci. 11(4), 1–23 (2015)MathSciNetCrossRefGoogle Scholar
  30. 30.
    Phillips, I., Ulidowski, I.: Operational semantics of reversibility in process algebra. In: APC, volume 162 of ENTCS, pp. 281–286 (2006)CrossRefGoogle Scholar
  31. 31.
    Phillips, I., Ulidowski, I.: Reversing algebraic process calculi. J. Log. Algebr. Methods Program. 73(1–2), 70–96 (2007)MathSciNetCrossRefGoogle Scholar
  32. 32.
    Phillips, I., Ulidowski, I.: Reversibility and asymmetric conflict in event structures. J. Log. Algebr. Methods Program. 84(6), 781–805 (2015)MathSciNetCrossRefGoogle Scholar
  33. 33.
    Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)zbMATHGoogle Scholar
  34. 34.
    Tiezzi, F., Yoshida, N.: Reversible session-based pi-calculus. J. Log. Algebr. Methods Program. 84(5), 684–707 (2015)MathSciNetCrossRefGoogle Scholar
  35. 35.
    Tiezzi, F., Yoshida, N.: Reversing single sessions. In: RC, volume 9720 of LNCS, pp. 52–69. Springer (2016)Google Scholar
  36. 36.
    Vieira, H.T., Caires, L., Seco, J.C.: The conversation calculus: a model of service-oriented computation. In: ESOP, volume 4960 of LNCS, pp. 269–283. Springer (2008)Google Scholar
  37. 37.
    Winskel, G.: Events in Computation. PhD thesis, Department of Computer Science, University of Edinburgh (1980)Google Scholar

Copyright information

© Springer-Verlag GmbH Germany, part of Springer Nature 2019

Authors and Affiliations

  1. 1.INRIAUniversité Côte d’AzurSophia AntipolisFrance
  2. 2.Dipartimento di InformaticaUniversità di TorinoTurinItaly
  3. 3.DiSITUniversità del Piemonte OrientaleAlessandriaItaly

Personalised recommendations