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

Robin Kaarsgaard, Niccolò Veltri

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


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.

TitelMathematics of Program Construction- 13th International Conference, MPC 2019, Proceedings
RedaktørerGraham Hutton
ISBN (Trykt)9783030336356
StatusUdgivet - 2019

Bibliografisk 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.


Dyk ned i forskningsemnerne om 'En Garde! Unguarded Iteration for Reversible Computation in the Delay Monad'. Sammen danner de et unikt fingeraftryk.