Reversible computing has a long history. Nowadays, reversible computing is attracting increasing interest because of its potential applications in diverse fields, including hardware design, biological modelling, program debugging and testing and quantum computing. Of particular interest is the application of reversible computation notions to the study of programming abstractions for dependable systems, because several techniques used to build dependable systems rely on some forms of undo or rollback. We continue, in this thesis, the study undertaken on reversible CCS by Vincent Danos and Jean Krivine, by defining a reversible higher-order pi-calculus (rhopi). We prove that reversibility in our calculus is causally consistent and that one can encode faithfully rhopi into a variant of HOpi. Moreover we design a fine-grained rollback primitive able to control the rollback of a concurrent execution. We give a formal specification of this primitive and show that it enjoys good properties, even in presence of concurrent conflicting rollbacks. We then devise a concurrent algorithm implementing such primitive and show that the algorithm respects the defined semantics.
