Compliance for reversible client/server interactions

Franco Barbanera
(Dipartimento di Matematica e Informatica, University of Catania)
Mariangiola Dezani-Ciancaglini
(Dipartimento di Informatica, University of Torino)
Ugo de' Liguoro
(Dipartimento di Informatica, University of Torino)

In the setting of session behaviours, we study an extension of the concept of compliance when a disciplined form of backtracking is present. After adding checkpoints to the syntax of session behaviours, we formalise the operational semantics via a LTS, and define a natural notion of checkpoint compliance. We then obtain a co-inductive characterisation of such compliance relation, and an axiomatic presentation that is proved to be sound and complete. As a byproduct we get a decision procedure for the new compliance, being the axiomatic system algorithmic.

In Marco Carbone: Proceedings Third Workshop on Behavioural Types (BEAT 2014), Rome, Italy, 1st September 2014, Electronic Proceedings in Theoretical Computer Science 162, pp. 35–42.
Published: 24th August 2014.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: