Semantic parametricity in polymorphic lambda calculus
Peter J. Freyd, Jean-Yves Girard, Andre Scedrov, Philip James Scott · 2003
A semantic condition necessary for the parametricity of polymorphic functions is considered. One of its instances is the stability condition for elements of variable type in the coherent domains semantics. A larger setting is presented that does not use retract pairs and keeps intact a basic feature of a certain function-type constructor. Polymorphic lambda terms are semantically parametric because of normalization.>