Reversibility in the higher-order π-calculus

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 pi-calculus, called rho pi. We prove that reversibility in our calculus is causally consistent and that the causal information used to support reversibility in rhos is consistent with the one used in the causal semantics of the pi-calculus developed by Boreale and Sangiorgi. Finally, we show that one can faithfully encode rho pi into a variant of higher-order pi, substantially improving on the result we obtained in the conference version of this paper. (C) 2016 Elsevier B.V. All rights reserved.