From reversible programming languages to reversible metalanguages

Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt

Standard

From reversible programming languages to reversible metalanguages. / Glück, Robert; Kaarsgaard, Robin; Yokoyama, Tetsuo.

I: Theoretical Computer Science, Bind 920, 2022, s. 46-63.

Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt

Harvard

Glück, R, Kaarsgaard, R & Yokoyama, T 2022, 'From reversible programming languages to reversible metalanguages', Theoretical Computer Science, bind 920, s. 46-63. https://doi.org/10.1016/j.tcs.2022.02.024

APA

Glück, R., Kaarsgaard, R., & Yokoyama, T. (2022). From reversible programming languages to reversible metalanguages. Theoretical Computer Science, 920, 46-63. https://doi.org/10.1016/j.tcs.2022.02.024

Vancouver

Glück R, Kaarsgaard R, Yokoyama T. From reversible programming languages to reversible metalanguages. Theoretical Computer Science. 2022;920:46-63. https://doi.org/10.1016/j.tcs.2022.02.024

Author

Glück, Robert ; Kaarsgaard, Robin ; Yokoyama, Tetsuo. / From reversible programming languages to reversible metalanguages. I: Theoretical Computer Science. 2022 ; Bind 920. s. 46-63.

Bibtex

@article{4aa617ae469649d2a03f281f1e27c891,

title = "From reversible programming languages to reversible metalanguages",

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.",

keywords = "Formal semantics, Iteration, Partial injective functions, Recursion, Reversible programming",

author = "Robert Gl{\"u}ck and Robin Kaarsgaard and Tetsuo Yokoyama",

note = "Publisher Copyright: {\textcopyright} 2022 Elsevier B.V.",

year = "2022",

doi = "10.1016/j.tcs.2022.02.024",

language = "English",

volume = "920",

pages = "46--63",

journal = "Theoretical Computer Science",

issn = "0304-3975",

publisher = "Elsevier",

}

RIS

TY - JOUR

T1 - From reversible programming languages to reversible metalanguages

AU - Glück, Robert

AU - Kaarsgaard, Robin

AU - Yokoyama, Tetsuo

PY - 2022

Y1 - 2022

N2 - 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.

AB - 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.

KW - Formal semantics

KW - Iteration

KW - Partial injective functions

KW - Recursion

KW - Reversible programming

U2 - 10.1016/j.tcs.2022.02.024

DO - 10.1016/j.tcs.2022.02.024

M3 - Journal article

AN - SCOPUS:85125445401

VL - 920

SP - 46

EP - 63

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

ER -

ID: 307745540