Reversibility in the higher-order π-calculus

Ivan Lanese 1, 2 Claudio Antares Mezzina 3 Jean-Bernard Stefani 4
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
4 SPADES - Sound Programming of Adaptive Dependable Embedded Systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : The notion of reversible computation is attracting increasing interest because of its applications in diverse fields, in particular the study of programming abstractions for reliable systems. In this paper, we continue the study undertaken by Danos and Krivine on reversible CCS by defining a reversible higher-order π-calculus, called rhoπ. We prove that reversibility in our calculus is causally consistent and that the causal information used to support reversibility in rhoπ is consistent with the one used in the causal semantics of the π-calculus developed by Boreale and Sangiorgi. Finally, we show that one can faithfully encode rhoπ into a variant of higher-order π, substantially improving on the result we obtained in the conference version of this paper.
Liste complète des métadonnées

Littérature citée [74 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01303090
Contributeur : Jean-Bernard Stefani <>
Soumis le : vendredi 15 avril 2016 - 19:24:38
Dernière modification le : jeudi 11 octobre 2018 - 08:48:04
Document(s) archivé(s) le : mardi 15 novembre 2016 - 04:53:16

Fichier

journal-rhopi.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Relations

Citation

Ivan Lanese, Claudio Antares Mezzina, Jean-Bernard Stefani. Reversibility in the higher-order π-calculus. Theoretical Computer Science, Elsevier, 2016, 625, pp.25-84. 〈10.1016/j.tcs.2016.02.019〉. 〈hal-01303090〉

Partager

Métriques

Consultations de la notice

179

Téléchargements de fichiers

94