From reversible programming languages to reversible metalanguages

Robert Glück, Robin Kaarsgaard, Tetsuo Yokoyama

Research output: Contribution to journalJournal articleResearchpeer-review

Abstract

During the past decade reversible programming languages have been formalized using various established semantics frameworks. However, these semantics fail to effectively specify the distinct properties of reversible languages at the metalevel, even including the central question of whether the defined language is reversible. In this paper, we build a metalanguage foundation for reversible languages from categorical principles, based on the category of sets and partial injective functions. We exemplify our approach by a step-by-step development of the full semantics of an r-Turing complete reversible while-language with recursive procedures. The use of the metalanguage leads to a formalization of the reversible semantics. A language defined in the metalanguage is guaranteed to have reversibility and inverse semantics. Also, program inverters for this language are obtained for free. We further discuss applications and directions for reversible semantics.
Original languageEnglish
JournalTheoretical Computer Science
Volume920
Pages (from-to)46-63
ISSN0304-3975
DOIs
Publication statusPublished - 12. Jun 2022
Externally publishedYes

Fingerprint

Dive into the research topics of 'From reversible programming languages to reversible metalanguages'. Together they form a unique fingerprint.

Cite this