Claudio Mezzina (INRIA)

Reversing Higher Order Pi

The notion of reversible computation is attracting increasing interest because of its potential applications in diverse fields. Of particular interest is the application of reversible computation ideas to the study of programming abstractions for reliable systems. In this paper, we continue the study undertaken by Danos and Krivine on reversible CCS by devising a simple syntax and reduction semantics for a reversible HOpi$ calculus, with a novel way of defining reversible reductions that preserves the associativity and commutativity of the parallel operator. We prove that reversibility in our calculus is causally consistent and that one can encode faithfully reversible HOpi into a variant of HOpi