En Garde! Unguarded Iteration for Reversible Computation in the Delay Monad

Robin Kaarsgaard, Niccolò Veltri

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

Abstract

Reversible computation studies computations which exhibit both forward and backward determinism. Among others, it has been studied for half a century for its applications in low-power computing, and forms the basis for quantum computing. Though certified program equivalence is useful for a number of applications (e.g., certified compilation and optimization), little work on this topic has been carried out for reversible programming languages. As a notable exception, Carette and Sabry have studied the equivalences of the finitary fragment of a reversible combinator calculus, yielding a two-level calculus of type isomorphisms and equivalences between them. In this paper, we extend the two-level calculus of finitary to one for full (i.e., with both recursive types and iteration by means of a trace combinator) using the delay monad, which can be regarded as a “computability-aware” analogue of the usual maybe monad for partiality. This yields a calculus of iterative (and possibly non-terminating) reversible programs acting on user-defined dynamic data structures together with a calculus of certified program equivalences between these programs.

Original languageEnglish
Title of host publicationMathematics of Program Construction- 13th International Conference, MPC 2019, Proceedings
EditorsGraham Hutton
Publication date2019
Pages366-384
ISBN (Print)9783030336356
DOIs
Publication statusPublished - 2019

Bibliographical note

DBLP's bibliographic metadata records provided through http://dblp.org/search/publ/api are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.

Keywords

  • Delay monad
  • Iteration
  • Reversible computation

Fingerprint

Dive into the research topics of 'En Garde! Unguarded Iteration for Reversible Computation in the Delay Monad'. Together they form a unique fingerprint.

Cite this