Transactions in RCCS

Vincent Danos, Jean Krivine

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We propose a formalisation of the notion of transaction, using a variant of CCS, RCCS, that distinguishes reversible and irreversible actions, and incorporates a distributed backtrack mechanism. Any weakly correct implementation of a transaction in CCS, once embedded in RCCS, automatically obtains a correct one. We show examples where this method allows for a more concise implementation and a simpler proof of correctness.
Original languageEnglish
Title of host publicationCONCUR 2005 – Concurrency Theory
Subtitle of host publication16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005. Proceedings
PublisherSpringer Physica
Number of pages15
ISBN (Electronic)978-3-540-31934-4
ISBN (Print)978-3-540-28309-6
Publication statusPublished - 2005

Publication series

NameLecture Notes in Computer Science

Cite this