Lanese, I.; Nishida, N.; Palacios, A.; Vidal, G. (2018). A theory of reversibility for Erlang. Journal of Logical and Algebraic Methods in Programming. 100:71-97. https://doi.org/10.1016/j.jlamp.2018.06.004
Por favor, use este identificador para citar o enlazar este ítem: http://hdl.handle.net/10251/145737
|
Title:
|
A theory of reversibility for Erlang
|
|
Author:
|
Lanese, Ivan
Nishida, Naoki
Palacios, Adrián
Vidal, Germán
|
|
UPV Unit:
|
Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació
|
|
Issued date:
|
|
|
Abstract:
|
[EN] 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 ...[+]
[EN] 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. (C) 2018 Elsevier Inc. All rights reserved.
[-]
|
|
Subjects:
|
Reversible computation
,
Actor model
,
Concurrency
,
Rollback recovery
|
|
Copyrigths:
|
Reconocimiento - No comercial - Sin obra derivada (by-nc-nd)
|
|
Source:
|
Journal of Logical and Algebraic Methods in Programming. (issn:
2352-2208
)
|
|
DOI:
|
10.1016/j.jlamp.2018.06.004
|
|
Publisher:
|
Elsevier
|
|
Publisher version:
|
https://doi.org/10.1016/j.jlamp.2018.06.004
|
|
Project ID:
|
info:eu-repo/grantAgreement/COST//IC1405/EU/Reversible computation - extending horizons of computing/
...[+]
info:eu-repo/grantAgreement/COST//IC1405/EU/Reversible computation - extending horizons of computing/
info:eu-repo/grantAgreement/MINECO//TIN2016-76843-C4-1-R/ES/Métodos rigurosos para el Internet del futuro/
info:eu-repo/grantAgreement/JSPS//JP17H01722/
info:eu-repo/grantAgreement/MINECO//EEBB-I-16-11469/ES/EEBB-I-16-11469/
info:eu-repo/grantAgreement/MINECO//TIN2013-44742-C4-1-R/ES/VALIDACION ASISTIDA DE PROGRAMAS MEDIANTE METODOS PRECISOS Y RIGUROSOS PARA UNA INGENIERIA DEL SOFTWARE ROBUSTA/
info:eu-repo/grantAgreement/MINECO//BES-2014-069749/ES/BES-2014-069749/
info:eu-repo/grantAgreement/GVA//PROMETEOII%2F2015%2F013/ES/SmartLogic: Logic Technologies for Software Security and Performance/
info:eu-repo/grantAgreement/MINECO//TIN2016-76843-C4-1-R/ES/METODOS RIGUROSOS PARA EL INTERNET DEL FUTURO/
[-]
|
|
Thanks:
|
This work has been partially supported by MINECO/AEI/FEDER (EU) under grants TIN2013-44742-C4-1-R and TIN2016-76843-C4-1-R, by the Generalitat Valenciana under grant PROMETEO-II/2015/013 (SmartLogic), by the COST Action ...[+]
This work has been partially supported by MINECO/AEI/FEDER (EU) under grants TIN2013-44742-C4-1-R and TIN2016-76843-C4-1-R, by the Generalitat Valenciana under grant PROMETEO-II/2015/013 (SmartLogic), by the COST Action IC1405 on Reversible Computation-extending horizons of computing, and by JSPS KAKENHI Grant Number JP17H01722. Adrian Palacios was partially supported by the EU (FEDER) and the Spanish Ayudas para contratos predoctorales para la formacian de doctores and Ayudas a la movilidad predoctoral para la realtzacion de estancias breves en centros de I+D, MINECO (SEIDI), under FPI grants BES-2014-069749 and EEBB-I-16-11469. Ivan Lanese was partially supported by INdAM as a member of GNCS (Gruppo Nazionale per il Calcolo Scientifico). Part of this research was done while the third and fourth authors were visiting Nagoya and Bologna Universities; they gratefully acknowledge their hospitality. Finally, we thank Salvador Tamarit and the anonymous reviewers for their helpful suggestions and comments.
[-]
|
|
Type:
|
Artículo
|
![[Cerrado]](/themes/UPV/images/candado.png)
