Transactions in RCCS

  • Krivine J
  • Danos V
  • 6


    Mendeley users who have this article in their library.
  • 52


    Citations of this article.


We propose a formalisation of the notion of transaction, using a variant of CCS, RCCS, that distinguishes reversible and irre- versible actions, and incorporates a distributed backtrack mechanism. Any weakly correct implementation of a transaction in CCS, once em- bedded in RCCS, automatically obtains a correct one.We show examples where this method allows for a more concise implementation and a sim- pler proof of correctness.

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document

  • ISSN: 03029743
  • SCOPUS: 2-s2.0-27244447468
  • PUI: 41520755
  • SGR: 27244447468


  • Jean Krivine

  • Vincent Danos

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free