Reversible Programs Have Reversible Semantics

Robert Glück, Robin Kaarsgaard, Tetsuo Yokoyama

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


During the past decade, reversible programming languages have been formalized using various established semantic frameworks. However, these semantics fail to effectively specify the distinct properties of reversible languages at the metalevel, and even neglect the central question of whether the defined language is reversible. In this paper, we build on a metalanguage foundation for reversible languages based on the category of sets and partial injective functions. We exemplify our approach through step-by-step development of the full semantics of an r-Turing complete reversible while-language with recursive procedures. This yields a formalization of the semantics in which the reversibility of the language and its inverse semantics are immediate, as well as the inversion of programs written in the language. We further discuss applications and future research directions for reversible semantics.

Original languageEnglish
Title of host publicationFormal Methods. FM 2019 International Workshops - Revised Selected Papers
EditorsEmil Sekerinski, Nelma Moreira, José N. Oliveira, Daniel Ratiu, Riccardo Guidotti, Marie Farrell, Matt Luckcuck, Diego Marmsoler, José Campos, Troy Astarte, Laure Gonnord, Antonio Cerone, Luis Couto, Brijesh Dongol, Martin Kutrib, Pedro Monteiro, David Delmas
Publication date2020
ISBN (Print)9783030549961
Publication statusPublished - 2020

Bibliographical note

DBLP's bibliographic metadata records provided through are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.


Dive into the research topics of 'Reversible Programs Have Reversible Semantics'. Together they form a unique fingerprint.

Cite this