Relative expressiveness of calculi for reversible concurrency

The main motivations for studying reversible computing comes from the promise that reversible computation (and circuits) would lead to more energy efficient computers. Besides circuits, nowadays, reversibility is studied in many other domains. This thesis studies the expressiveness of the causalconsistent reversibility (a well-known notion of reversibility for concurrent systems) in CCS and π-calculus. First, we show that by means of encodings, LTSs of Reversible CCS (introduced by Danos and Krivine) and CCS with Communications Keys (introduced by Phillips and Ulidowski) are isomorphic up to some structural transformations of processes. An explanation of this result is the existence of one causality notion in CCS. In π-calculus, two forms of dependences between the actions give rise to different causal semantics. The main difference is how the parallel extrusion of the same name is treated. We consider three approaches to parallel extrusion problem represented with causal semantics introduced by Boreale et al; Crafa et al; and Cristescu et al. To study them, we devise a framework for reversible π-calculi, parametric with respect to the data structure used to keep track of information about a name extrusions. We show that reversibility induced by our framework is causally-consistent and prove causal correspondence between the semantics given by Boreale et al, and the corresponding instance of the framework.