Join inverse rig categories for reversible functional programming, and beyond

Robin Kaarsgaard, Mathys Rennela

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

15 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.
Original languageEnglish
Title of host publicationProceedings 37th Conference on Mathematical Foundations of Programming Semantics
EditorsAna Sokolova
Volume351
Publication date2021
Pages152-167
DOIs
Publication statusPublished - 2021
Externally publishedYes
Event37th Conference on Mathematical Foundations of Programming Semantics - Hybrid, Salsburg, Austria
Duration: 30. Aug 20212. Sept 2021

Conference

Conference37th Conference on Mathematical Foundations of Programming Semantics
LocationHybrid
Country/TerritoryAustria
CitySalsburg
Period30/08/202102/09/2021
SeriesElectronic Proceedings in Theoretical Computer Science
Volume351
ISSN2075-2180

Fingerprint

Dive into the research topics of 'Join inverse rig categories for reversible functional programming, and beyond'. Together they form a unique fingerprint.

Cite this