A Small-Step Semantics for Janus

Janus is an imperative, sequential language for reversibility. While heavily studied in the reversibility literature, to the best of our knowledge, no small-step semantics for it exists. Hence, we propose a small-step semantics for Janus and we prove it equivalent to a big-step semantics from the literature, for programs that have no runtime errors and no divergence. Our main motivation is to enable a future extension of Janus with concurrency primitives, which is more easily defined on top of a small-step semantics. As additional feature, a small-step semantics allows one to more easily distinguish between failing and non-terminating computations.