Sequence Types for the π-calculus

We introduce channel sequence types to study finitary polymorphism in the context of mobile processes modelled in the π-calculus. We associate to each channel a set of exchange types, and we require that output processes send values of one of those types, and input processes accept values of any type in the set. Our type assignment system enjoys subject reduction and guarantees the absence of communication errors. We give several examples of polymorphism, and we encode the λ-calculus with the strict intersection type discipline.