# A Reversible Semantics for Janus

arXiv: https://arxiv.org/abs/2602.16913 · HTML: https://mlsanity.com/paper/2602.16913/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 2 of its 33 references that are in the map.
- First posted on arXiv 18 Feb 2026.

## Builds on (most cited first, 2 of 2)

- [A Theory of Reversibility for Erlang](https://mlsanity.com/paper/1806.07100/) (2018)
- [Design and Implementation of a Reversible Object-Oriented Programming Language](https://mlsanity.com/paper/1707.07845/) (2017)

## Abstract (arXiv)

Janus is a paradigmatic example of a reversible programming language. Indeed, Janus programs can be executed backwards as well as forwards. However, its current 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 a 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.