Behavioural analysis of sessions using the calculus of structures

Ciobanu, Gabriel and Horne, Ross; Mazzara, Manuel and Voronkov, Andrei, eds. (2016) Behavioural analysis of sessions using the calculus of structures. In: Perspectives of System Informatics. Lecture Notes in Computer Science . Springer, Cham, pp. 91-106. ISBN 9783319415796 (https://doi.org/10.1007/978-3-319-41579-6_8)

[thumbnail of Ciobanu-Horne-PSI-2016-Behavioural-analysis-of-sessions-using-the-calculus-of-structures]
Preview
 Text. Filename: Ciobanu-Horne-PSI-2016-Behavioural-analysis-of-sessions-using-the-calculus-of-structures.pdf
Accepted Author Manuscript
License: Strathprints license 1.0
Download (657kB)| Preview

Abstract

This paper describes an approach to the behavioural analysis of sessions. The approach is made possible by the calculus of structures — a deep inference proof calculus, generalising the sequent calculus, where inference rules are applied in any context. The approach involves specifications of global and local sessions inspired by the Scribble language. The calculus features a novel operator that synchronises parts of a protocol that must be treated atomically. Firstly, the calculus can be used to determine whether local sessions can be compose in a type safe fashion such that sessions are capable of successfully completing. Secondly, the calculus defines a subtyping relation for sessions that allows causal dependencies to be weakened while retaining termination potential. Consistency and complexity results follow from proof theory.

CORE (COnnecting REpositories)