Reversible sessions with flexible choices (Q2329306)

This paper presents and studies a type system for reversible communication protocols. In particular, the main purpose of the session-type inspired system is to structure and enforce multiple properties on a reversible concurrent calculus endowed with a ``flexible'' choice operator. In addition to forward ``expected'' properties, such as subject reduction and progress, their reversible counterparts are also proven to hold, along with a ``session fidelity'' property. As the authors detail in the ``Related work and conclusion'' section, the calculus under study is a patchwork of good ideas: they adopt a ``static'' rollback operator that carries the memory of previous failures; represents both internal and external choices; makes the distinction between user processes and runtime processes. This gives an interesting rule BackA that ``throws away'' the branch on which the process wants to backtrack, while maintaining causal consistency, but at the cost of the loop lemma. Their session type system takes inspiration from existing approaches when it labels the choice operators with checkpoints, but also introduces novelty, e.g., by studying the interplay of (a relaxed version of) connecting actions with reversible computation. This blend of choices gives an interesting, technical and original paper that manages to make a difficult topic accessible. The interplay between connecting communications and reversibility makes some parts of the paper tedious, but the level of rigor maintained all along helps build trust in this interesting paper that tackles a difficult problem.