(Web Services Calculus)
WS-CALCULUS formalizes the semantics of an expressive subset of WS-BPEL, with special concern for modeling the interactions among web services, be them WS-BPEL processes or not, in a network context. This allows us to tackle those problems arising when executing WS-BPEL processes, such as multiple start activities, receive conflicts, routing of messages, while avoiding the intricacies of dealing with any, possibly redundant, WS-BPEL construct. We also define a type system for WS-CALCULUS terms, that enforces many of the constraints imposed by WSDL/WS-BPEL, e.g. it prevents programs from passing links that have been implicitly initialized and from invoking callback operations that do not have previous triggering receive operations. However, in some cases it is even further restrictive so to enforce a more disciplined programming style.