Static versus dynamic reversibility in CCS (Q2022303)

This paper is interested in the comparison of two different systems to represent concurrent and reversible computation, RCCS and CCSK. As the authors note in the conclusion, ``while the number of concurrent reversible calculi and languages is increasing, there is very little literature on the relations between them.'' This is unfortunate, as the proliferation can sometimes hide the commonalities and hinder global progress. The two mentioned systems were born with the same goals and similar methodologies, but made different choices as to how the memory of past actions should be stored: on an independent stack for RCCS, or ``embedded'' in the term for CCSK. It has always been suspected that the two calculi were equivalent in a strong sense, and this is what this paper proves, but, as often with ``folklore results'', a lot of work and clarifications were needed to reach this point. Fortunately, the authors carry on this task with a lot of clarity and explanations, making it a pleasure to read their contribution. Among the benefits of this paper lies a certain ``standardization'' of RCCS and CSSK: both calculi have evolved over the time, and this paper takes the time to lay out the systems without ambiguity. Among other variations, RCCS's alpha-conversion and CCSK's tau prefixes are discussed and design choices are made. One of the difficulties of the result is that RCCS's structural congruence is always ``in the way'' of the reductions, and needs a particular treatment, something the authors do with clarity and care. This paper is a must-read for anyone interested in working with either system or curious about possible development for name-passing reversible operator algebra. It is interesting to note that the paper uses a notion of context (p.~11 and p.~20), with and without history: contexts were recently re-investigated in the context of (variations of) RCCS and CCSK, and, surprisingly, led to opposite results [\textit{I. Lanese} and \textit{I. Phillips}, Lect. Notes Comput. Sci. 12805, 126--143 (2021; Zbl 1476.68097); \textit{C. Aubert} and \textit{D. Medić}, ibid. 12805, 144--162 (2021; Zbl 1476.68093)]. This may be the sign that another paper of the same caliber is needed to restore the mapping between the systems, or that, despite this sound result, the two systems are kind on diverging on their extensions.