General Terms Theory, Languages

Abstract. We define and study parametric polymorphism for a type system with recursive, product, union, intersection, negation, and function types. We first recall why the definition of such a sys-tem was considered hard—when not impossible—and then present the main ideas at the basis of our solution. In particular, we intro-duce the notion of “convexity ” on which our solution is built up and discuss its connections with parametricity as defined by Reynolds to whose study our work sheds new light