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.-B. (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.| File | Dimensione | Formato | |
|---|---|---|---|
|
main.pdf
Open Access dal 29/05/2025
Descrizione: Postprint autore
Tipo:
Postprint / Author's Accepted Manuscript (AAM) - versione accettata per la pubblicazione dopo la peer-review
Licenza:
Licenza per accesso libero gratuito
Dimensione
575.38 kB
Formato
Adobe PDF
|
575.38 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
