A Per Model of Polymorphism and Recursive Types

Abstract

A model of Reynolds’ polymorphic lambda calculus is provided, which also allows the recursive definition of elements and types. The technique is to use a good class of partial equivalence relations over a certain cpo. This allows the combination of inverse-limits for recursion and intersection for polymorphism.