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.
Lami, P., Lanese, I., Stefani, J.-. (2024). A Small-Step Semantics for Janus. GEWERBESTRASSE 11, CHAM, CH-6330, SWITZERLAND : Springer Science and Business Media Deutschland GmbH [10.1007/978-3-031-62076-8_8].
A Small-Step Semantics for Janus
Lami P.;Lanese I.;
2024
Abstract
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
