Recursive types for Fun

AbstractThe language Fun [13] is a typed polymorphic lambda calculus with a notion of subtyping and quantifiers ranging over subtypes of a given type. In this paper we show that it is consistent to allow recursive type definitions in Fun, by constructing an interpretation of types as partial equivalence relations of a special kind, terms being interpreted as equivalence classes, modulo such relations, of elements of a model for an underlying untyped language