Programming news · October 2025
New semantics treats reversible computation as ordinary causal computation
In “Reversible computations are computations,” Clément Aubert and Jean Krivine generalise configuration structures and prime event structures — the standard causal models for concurrent systems — so that they naturally accommodate events that can be undone.
They define a computation as valid when each observed event is preceded by the observation of its causes, and introduce a symmetric residuation operation under which stable structures remain stable. Their central insight is that reversible semantics corresponds to a switch operation exchanging the roles of conflict and causality, suggesting reversibility is not an exotic add-on but a structural symmetry already latent in concurrency theory.
Firmer theoretical foundations help reversible languages and debuggers reason correctly about distributed and concurrent programs that can run backward.