A PER model of polymorphism and recursive types
M. Abadi, Gordon D. Plotkin · 2002
A model of Reynold's polymorphic lambda calculus is provided, which also allows the recursive definition of elements and types. The techniques uses a good class of partial equivalence relations (PERs) over a certain CPO. This allows the combination of inverse-limits for recursion and intersection for polymorphism.>