Encoding CDuce in the Cπ-calculus

We present a type faithful encoding of CDuce into the C pi-calculus. These calculi are two variants of, respectively, the X-calculus and the pi-calculus, characterised by rich typing and subtyping systems with union, negation, and intersection types. The encoding is interesting because it sheds new light on the Milner-Turner encoding, on the relations between sequential and remote execution of functions/services, and on the validity of the equational laws for union and intersection types in pi-calculus.