2011 | OriginalPaper | Chapter
Controlling Reversibility in Higher-Order Pi
Authors : Ivan Lanese, Claudio Antares Mezzina, Alan Schmitt, Jean-Bernard Stefani
Published in: CONCUR 2011 – Concurrency Theory
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. 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.