Join Inverse Rig Categories for Reversible Functional Programming, and Beyond

DOI10.4204/EPTCS.351.10arXiv2105.09929MaRDI QIDQ6368151FDOQ6368151

Authors: Robin Kaarsgaard, Mathys Rennela 

Publication date: 20 May 2021

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.

This page was built for publication: Join Inverse Rig Categories for Reversible Functional Programming, and Beyond

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6368151)