Instant Polymorphic Type Systems for Mobile Process Calculi: Just Add Reduction Rules and Stir

J. B. Wells and Henning Makholm, Heriot-Watt University

Many different mobile process calculi have been invented, and for each some number of type systems has been developed. Soundness and other properties must be proved separately for each calculus and type system.

We present ongoing work on developing a 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.