Reversible programs have reversible semantics

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningfagfællebedømt

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.

OriginalsprogEngelsk
TitelFormal Methods. FM 2019 International Workshops - Revised Selected Papers
RedaktørerEmil 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
ForlagSpringer VS
Publikationsdato2020
Sider413-427
ISBN (Trykt)9783030549961
DOI
StatusUdgivet - 2020
Begivenhed3rd World Congress on Formal Methods, FM 2019 - Porto, Portugal
Varighed: 7 okt. 201911 okt. 2019

Konference

Konference3rd World Congress on Formal Methods, FM 2019
LandPortugal
ByPorto
Periode07/10/201911/10/2019
NavnLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Vol/bind12233 LNCS
ISSN0302-9743

ID: 248898134