Reversible Multiparty Sessions with Checkpoints

Mariangiola Dezani-Ciancaglini
(Dipartimento di Informatica, Universita' di Torino)
Paola Giannini
(Computer Science Institute, DiSIT, Universita' del Piemente Orientale)

Reversible interactions model different scenarios, like biochemical systems and human as well as automatic negotiations. We abstract interactions via multiparty sessions enriched with named checkpoints. Computations can either go forward or roll back to some checkpoints, where possibly different choices may be taken. In this way communications can be undone and different conversations may be tried. Interactions are typed with global types, which control also rollbacks. Typeability of session participants in agreement with global types ensures session fidelity and progress of reversible communications.

In Daniel Gebler and Kirstin Peters: Proceedings Combined 23rd International Workshop on Expressiveness in Concurrency and 13th Workshop on Structural Operational Semantics (EXPRESS/SOS 2016), Québec City, Canada, 22nd August 2016, Electronic Proceedings in Theoretical Computer Science 222, pp. 60–74.
Published: 9th August 2016.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: