XPi: A typed process calculus for XML messaging

We present XPi, a core calculus for XML messaging. XPi features asynchronous communication, pattern matching, name and code mobility, integration of static and dynamic typing. In XPi, a type system disciplines XML message handling at the level of channels, patterns, and processes. A run-time safety theorem ensures that in well-typed systems no service will ever receive documents it cannot understand, and that the offered services will be consistent with the declared channel capacities. An inference system is introduced, which is proved to be in full agreement with type checking. A notion of barbed equivalence is defined that takes into account information about service interfaces. Flexibility and expressiveness of this calculus are illustrated by a number of examples, some concerning description and discovery of web services.