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
Standard
En Garde! Unguarded Iteration for Reversible Computation in the Delay Monad. / Kaarsgaard, Robin; Veltri, Niccolò.
Mathematics of Program Construction- 13th International Conference, MPC 2019, Proceedings. ed. / Graham Hutton. Springer VS, 2019. p. 366-384 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 11825 LNCS).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - En Garde! Unguarded Iteration for Reversible Computation in the Delay Monad
AU - Kaarsgaard, Robin
AU - Veltri, Niccolò
PY - 2019
Y1 - 2019
N2 - 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.
AB - 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.
KW - Delay monad
KW - Iteration
KW - Reversible computation
UR - http://www.scopus.com/inward/record.url?scp=85076114425&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-33636-3_13
DO - 10.1007/978-3-030-33636-3_13
M3 - Article in proceedings
AN - SCOPUS:85076114425
SN - 9783030336356
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 366
EP - 384
BT - Mathematics of Program Construction- 13th International Conference, MPC 2019, Proceedings
A2 - Hutton, Graham
PB - Springer VS
T2 - 13th International Conference on Mathematics of Program Construction, MPC 2019
Y2 - 7 October 2019 through 9 October 2019
ER -
ID: 237703180