2016/06/20 by Claudio A. Mezzina, Jorge A. Pérez
Computer Science · #cs.LO #cs.PL
paper · pdf · doi:10.4204/eptcs.211.6
published as EPTCS 211, 2016, pp. 56-64 · In Proceedings PLACES 2016, arXiv:1606.05403
arxiv created 2016/06/20 · arxiv updated 2016/06/21
Much research has studied foundations for correct and reliable communication-centric systems. A salient approach to correctness uses session types to enforce structured communications; a recent approach to reliability uses reversible actions as a way of reacting to unanticipated events or failures. This note develops a simple observation: the machinery required to define asynchronous semantics and monitoring can also support reversible protocols. We propose a process framework of session communication in which monitors support reversibility. A key novelty in our approach are session types with present and past, which allow us to streamline the semantics of reversible actions.