We present the generic polymorphic type system Poly which works for a wide range of mobile process calculi. For any calculus satisfying some general syntactic conditions, well-formedness rules for types are derived automatically from the reduction rules and Poly works otherwise unchanged. The derived type system is automatically sound and often more precise than previous type systems for the calculus, due to Poly's spatial polymorphism.
We present an implemented type inference algorithm for Poly which automatically constructs a typing given a set of reduction rules and a term to be typed. The generated typings are principal with respect to certain natural type shape constraints.