En Garde! Unguarded Iteration for Reversible Computation in the Delay Monad
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-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.
Original language | English |
---|---|
Title of host publication | Mathematics of Program Construction- 13th International Conference, MPC 2019, Proceedings |
Editors | Graham Hutton |
Publisher | Springer VS |
Publication date | 2019 |
Pages | 366-384 |
ISBN (Print) | 9783030336356 |
DOIs | |
Publication status | Published - 2019 |
Event | 13th International Conference on Mathematics of Program Construction, MPC 2019 - Porto, Portugal Duration: 7 Oct 2019 → 9 Oct 2019 |
Conference
Conference | 13th International Conference on Mathematics of Program Construction, MPC 2019 |
---|---|
Land | Portugal |
By | Porto |
Periode | 07/10/2019 → 09/10/2019 |
Series | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 11825 LNCS |
ISSN | 0302-9743 |
- Delay monad, Iteration, Reversible computation
Research areas
ID: 237703180