2014/06/13 by Francesco Tiezzi, Nobuko Yoshida
Computer Science · #cs.PL #cs.LO #cs.SE
paper · pdf · doi:10.4204/eptcs.155.3
published as EPTCS 155, 2014, pp. 17-24 · In Proceedings PLACES 2014, arXiv:1406.3313
arxiv created 2014/06/13 · arxiv updated 2014/06/16
In this work, we incorporate reversibility into structured communication-based programming, to allow parties of a session to automatically undo, in a rollback fashion, the effect of previously executed interactions. This permits taking different computation paths along the same session, as well as reverting the whole session and starting a new one. Our aim is to define a theoretical basis for examining the interplay in concurrent systems between reversible computation and session-based interaction. We thus enrich a session-based variant of pi-calculus with memory devices, dedicated to keep track of the computation history of sessions in order to reverse it. We discuss our initial investigation concerning the definition of a session type discipline for the proposed reversible calculus, and its practical advantages for static verification of safe composition in communication-centric distributed software performing reversible computations.