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

TL;DR
This paper introduces a formal framework for reversible multiparty communication sessions with checkpoints, enabling interactions to be undone or revisited, ensuring reliable and flexible communication protocols.
Contribution
It extends multiparty session types with checkpoints and rollback capabilities, providing a typed model that guarantees session fidelity and progress in reversible interactions.
Findings
Model supports rollback to checkpoints in multiparty sessions
Type system ensures session fidelity and progress
Enables flexible interaction scenarios like negotiations
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
