From reversible programming languages to reversible metalanguages

Research output: Contribution to journalJournal articleResearchpeer-review

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
Number of pages18
ISSN0304-3975
DOIs
Publication statusPublished - 2022

Bibliographical note

Publisher Copyright:
© 2022 Elsevier B.V.

    Research areas

  • Formal semantics, Iteration, Partial injective functions, Recursion, Reversible programming

ID: 307745540