Join inverse rig categories for reversible functional programming, and beyond

Robin Kaarsgaard, Mathys Rennela

Publikation: Kapitel i bog/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

19 Downloads (Pure)

Abstract

Reversible computing is a computational paradigm in which computations are deterministic in both the forward and backward direction, so that programs have well-defined forward and backward semantics. We investigate the formal semantics of the reversible functional programming language Rfun. For this purpose we introduce join inverse rig categories, the natural marriage of join inverse categories and rig categories, which we show can be used to model the language Rfun, under reasonable assumptions. These categories turn out to be a particularly natural fit for reversible computing as a whole, as they encompass models for other reversible programming languages, notably Theseus and reversible flowcharts. This suggests that join inverse rig categories really are the categorical models of reversible computing.
OriginalsprogEngelsk
TitelProceedings 37th Conference on Mathematical Foundations of Programming Semantics
RedaktørerAna Sokolova
Vol/bind351
Publikationsdato2021
Sider152-167
DOI
StatusUdgivet - 2021
Udgivet eksterntJa
Begivenhed37th Conference on Mathematical Foundations of Programming Semantics - Hybrid, Salsburg, Østrig
Varighed: 30. aug. 20212. sep. 2021

Konference

Konference37th Conference on Mathematical Foundations of Programming Semantics
LokationHybrid
Land/OmrådeØstrig
BySalsburg
Periode30/08/202102/09/2021
NavnElectronic Proceedings in Theoretical Computer Science
Vol/bind351
ISSN2075-2180

Fingeraftryk

Dyk ned i forskningsemnerne om 'Join inverse rig categories for reversible functional programming, and beyond'. Sammen danner de et unikt fingeraftryk.

Citationsformater