Behavioural analysis of sessions using the calculus of structures

Gabriel Ciobanu, Ross Horne

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

7 Citations (Scopus)
14 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationPerspectives of System Informatics
Subtitle of host publication10th International Andrei Ershov Informatics Conference, PSI 2015, in Memory of Helmut Veith
EditorsManuel Mazzara, Andrei Voronkov
Place of PublicationCham
PublisherSpringer
Pages91-106
Number of pages16
ISBN (Electronic)9783319415796
ISBN (Print)9783319415789
DOIs
Publication statusPublished - 28 Jun 2016

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume9609
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Keywords

  • local type
  • linear logic
  • parallel composition
  • local protocol
  • causal dependency

Fingerprint

Dive into the research topics of 'Behavioural analysis of sessions using the calculus of structures'. Together they form a unique fingerprint.

Cite this