Subtyping relations for the pi-calculus are usually defined in a syntactic way, by means of structural rules. We propose a semantic characterisation of channel types and use it to derive a subtyping relation.

The type system we consider includes read-only and write-only channel types, as well as boolean combinations of types. A set-theoretic interpretation of types is provided, in which boolean combinations are interpreted as the corresponding set-theoretic operations. Subtyping is defined as inclusion of the interpretations. The resulting subtyping relation is decidable.

In order to fully exploit the type system, we define a variant of the pi-calculus, called the Cpi-calculus, where communication is subjected to pattern matching that performs dynamic typecase.

This paves the way toward a novel integration of functional and concurrent features, obtained by combining the pi-calculus with CDuce, a functional programming language for XML manipulation that is based on semantic subtyping. More information on CDuce, its theory and its development, can be found at www.cduce.org.

If time permits I will sketch a "local" version of our calculus, and I will present the problems that arise when one tries to encode CDuce in Cpi.

This is joint work with Giuseppe Castagna and Rocco de Nicola, and will be presented in a paper at LICS 2005.