A Graphical Approach to Progress for Structured Communication in Web Services

TL;DR

This paper introduces a graphical method to analyze progress in session-based web services, showing that acyclic dependency graphs ensure reducibility and progress in well-typed processes, with implications for modern programming languages.

Contribution

It presents a graphical approach to prove progress in session-typed pi-calculus processes, including higher-order sessions and delegation, ensuring acyclicity preserves reducibility.

Findings

Acyclic dependency graphs guarantee process reducibility.

Acyclicity is preserved under reduction for well-typed processes.

Transparent processes form a large class with practical applications.

Abstract

We investigate a graphical representation of session invocation interdependency in order to prove progress for the pi-calculus with sessions under the usual session typing discipline. We show that those processes whose associated dependency graph is acyclic can be brought to reduce. We call such processes transparent processes. Additionally, we prove that for well-typed processes where services contain no free names, such acyclicity is preserved by the reduction semantics. Our results encompass programs (processes containing neither free nor restricted session channels) and higher-order sessions (delegation). Furthermore, we give examples suggesting that transparent processes constitute a large enough class of processes with progress to have applications in modern session-based programming languages for web services.