Search papers, labs, and topics across Lattice.
This paper introduces a novel small-step semantics for the reversible programming language Janus that, unlike previous semantics, is itself reversible, satisfying the Loop Lemma. The new semantics addresses the challenge of defining a reversible small-step semantics based on a program counter for a high-level language, overcoming information loss during forward execution. The authors prove the equivalence of the new semantics to the original Janus semantics, thus preserving the language's original behavior.
A reversible small-step semantics for Janus finally makes debugging and concurrent extensions possible for this reversible language.
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.
