Toward a semantics for the QUEST language

A model is given for the second-order lambda calculus extended with inheritance, bounded quantification, recursive types, constructors and kinds. This language, called μ-FunK, can be viewed as the core of the QUEST language defined by L. Cardelli (SRC Rep. 45, 1989). Types are interpreted as intervals of partial equivalence relations. Because of the properties of intervals and their ordering, all the type constructors are continuous functions. As a consequence a system where a kind is given to each constructor constant employed can be modeled. In such a model the meaning of operator μ, the constructor of recursive types, turns out to be just the minimal fixed-point operator