From reversible programming languages to reversible metalanguages

Robert Glück, Robin Kaarsgaard, Tetsuo Yokoyama

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer 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.
TidsskriftTheoretical Computer Science
Sider (fra-til)46-63
StatusUdgivet - 12. jun. 2022
Udgivet eksterntJa