2011 | OriginalPaper | Buchkapitel
Controlling Reversibility in Higher-Order Pi
verfasst von : Ivan Lanese, Claudio Antares Mezzina, Alan Schmitt, Jean-Bernard Stefani
Erschienen in: CONCUR 2011 – Concurrency Theory
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We present in this paper a fine-grained rollback primitive for the higher-order
π
-calculus (HO
π
), that builds on the reversibility apparatus of reversible HO
π
[9]. The definition of a proper semantics for such a primitive is a surprisingly delicate matter because of the potential interferences between concurrent rollbacks. We define in this paper a high-level operational semantics which we prove sound and complete with respect to reversible HO
π
backward reduction. We also define a lower-level distributed semantics, which is closer to an actual implementation of the rollback primitive, and we prove it to be fully abstract with respect to the high-level semantics.