Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
6874815 | Journal of Logical and Algebraic Methods in Programming | 2018 | 27 Pages |
Abstract
In a reversible language, any forward computation can be undone by a finite sequence of backward steps. Reversible computing has been studied in the context of different programming languages and formalisms, where it has been used for testing and verifica- tion, among others. In this paper, we consider a subset of Erlang, a functional and concurrent programming language based on the actor model. We present a formal semantics for reversible computation in this language and prove its main properties, including its causal consistency. We also build on top of it a rollback operator that can be used to undo the actions of a process up to a given checkpoint.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Ivan Lanese, Naoki Nishida, Adrián Palacios, Germán Vidal,