A Reversible Semantics for Janus
This addresses a foundational issue in reversible programming languages, enabling debugging and concurrency extensions, though it is incremental as it builds on existing Janus semantics.
The authors tackled the problem that Janus's small-step semantics is not reversible, failing to satisfy the Loop Lemma, and presented a novel reversible small-step semantics that remains equivalent to the previous one.
Janus is a paradigmatic example of reversible programming language. Indeed, Janus programs can be executed backwards as well as forwards. However, its small-step semantics (useful, e.g., for debugging or as a basis for extensions with concurrency primitives) is not reversible, since it loses information while computing forwards. E.g., it does not satisfy the Loop Lemma, stating that any reduction has an inverse, a main property of reversibility in process calculi, where small-step semantics is commonly used. We present here a novel small-step semantics which is actually reversible, while remaining equivalent to the previous one. It involves the non-trivial challenge of defining a semantics based on a "program counter" for a high-level programming language.