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 verification, 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.

Lanese, I., Nishida, N., Palacios, A., Vidal, G. (2018). A theory of reversibility for Erlang. THE JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 100, 71-97 [10.1016/j.jlamp.2018.06.004].

A theory of reversibility for Erlang

Lanese, Ivan;
2018

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 verification, 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.
2018
Lanese, I., Nishida, N., Palacios, A., Vidal, G. (2018). A theory of reversibility for Erlang. THE JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 100, 71-97 [10.1016/j.jlamp.2018.06.004].
Lanese, Ivan; Nishida, Naoki; Palacios, Adrián; Vidal, Germán
File in questo prodotto:
File Dimensione Formato  
paper.pdf

Open Access dal 11/07/2020

Tipo: Postprint
Licenza: Licenza per accesso libero gratuito
Dimensione 1.4 MB
Formato Adobe PDF
1.4 MB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/674989
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 42
  • ???jsp.display-item.citation.isi??? 29
social impact