A Graphical Approach to Progress for Structured Communication in Web Services
arXiv:1010.5566 · doi:10.4204/EPTCS.38.4
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.
In Proceedings ICE 2010, arXiv:1010.5308
References in corpus (1)
Cited by in corpus (10)
- A Graphical Approach to Progress for Structured Communication in Web Services
- A Language for the Declarative Composition of Concurrent Protocols
- Comparing Deadlock-Free Session Typed Processes
- Separating Sessions Smoothly
- Type-checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion
- Session Types in a Linearly Typed Multi-Threaded Lambda-Calculus
- Prioritise the Best Variation
- Linearly Typed Dyadic Group Sessions for Building Multiparty Sessions
- Session Types with Runtime Adaptation: Overview and Examples
- Proceedings of the Combined 22th International Workshop on Expressiveness in Concurrency and 12th Workshop on Structural Operational Semantics