Genericity and the Pi-Calculus

Martin Berger, Kohei Honda, Nobuko Yoshida

We introduce a typed pi-calculus with generic interaction and
second-order quantification. Genericity is represented as generic
information flow among processes on which the type discipline enforces
strict duality and uniformity. This enables the calculus to accurately
capture and generalise functional genericity. This paper establishes
two fundamental results about the calculus: strong normalisability of
typed processes in the presence of second-order quantification and a
fully abstract embedding of System F, the second order polymorphic
lambda-calculus.