Session Types for Orchestrated Interactions

TL;DR

This paper introduces a novel approach to session types in pi-calculus by incorporating retractable compliance and speculative selection, enabling more flexible interactions and improved operational semantics.

Contribution

It extends session types with a new operator and an orchestrator-based semantics, relaxing duality constraints and enhancing communication flexibility.

Findings

Proposes a new type operator 'speculative selection'.

Develops an orchestrator-based operational semantics.

Provides a sound type system for the extended session types.

Abstract

In the setting of the pi-calculus with binary sessions, we aim at relaxing the notion of duality of session types by the concept of retractable compliance developed in contract theory. This leads to extending session types with a new type operator of "speculative selection" including choices not necessarily offered by a compliant partner. We address the problem of selecting successful communicating branches by means of an operational semantics based on orchestrators, which has been shown to be equivalent to the retractable semantics of contracts, but clearly more feasible. A type system, sound with respect to such a semantics, is hence provided.