Under a reversible semantics, computation steps can be undone. This paper
addresses the integration of reversible semantics into process languages for
communication-centric systems, equipped with behavioral types.
In prior work, we introduced a monitors-as-memories approach to seamlessly
integrate reversible semantics into a process model in which concurrency is
governed by session types (a class of behavioral types), covering binary
(two-party) protocols with synchronous communications. Although such a model
offers a simple setting for showcasing our approach, its expressiveness is
Here we substantially extend our approach, and use it to define reversible
semantics for a very expressive process model that accounts for multiparty
(n-party) protocols (choreographies), asynchronous communication, decoupled
rollbacks, and process passing. As main technical result, we prove that our
multiparty, reversible semantics is causally-consistent.