2026-07-22T18:26:01Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:8477 2024-03-06T10:39:28Z ddc:004 open_access

A Certified Study of a Reversible Programming Language Paolini, Luca Piccolo, Mauro Roversi, Luca reversible computing Janus operational semantics bi-deterministic evaluation categorical semantics We advance in the study of the semantics of Janus, a C-like reversible programming language. Our study makes utterly explicit some backward and forward evaluation symmetries. We want to deepen mathematical knowledge about the foundations and design principles of reversible computing and programming languages. We formalize a big-step operational semantics and a denotational semantics of Janus. We show a full abstraction result between the operational and denotational semantics. Last, we certify our results by means of the proof assistant Matita. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Luca Paolini and Mauro Piccolo and Luca Roversi 2018 Is Part Of LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2015.7 urn:nbn:de:0030-drops-84771 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.7 eng https://creativecommons.org/licenses/by/3.0/legalcode