A Graphical Approach to Progress for Structured Communication in Web Services
Source: University of Copenhagen
The authors investigate a graphical representation of session invocation interdependency in order to prove progress for the p-calculus with sessions under the usual session typing discipline. They show that those processes whose associated dependency graph is acyclic can be brought to reduce. They call such processes transparent processes. Additionally, they prove that for well-typed processes where services contain no free names, such acyclicity is preserved by the reduction semantics. The results encompass programs (processes containing neither free nor restricted session channels) and higher-order sessions (delegation).