The paper concentrates on the construction of a suitable semantics for the system F of variable types, that is, schemes of abstraction with respect to types. Since its formulation, the idea of variable types has become commonplace in computer science. There has not been much progress in the underlying theory, however, as the introduction of universal types created circularity problems in the calculus. A function of a universal type can be applied to any type without restriction, and this poses a problem analogous to the self-application paradoxes of the untyped theories.

In this paper, the author presents an attempt to fill the gap in the theory and to develop a semantics of the system of variable types. This semantics is based on the category-theoretic notion of direct limit, which allows us to describe the behavior of a variable type on any domain based on its behavior on finite domains. To do this, a new construct of the so-called qualitative domains is introduced, and the author demonstrates that it represents a refinement of Scott domains. The interpretation introduced for the system of variable types is also used to define a small universal model of lambda calculus yielding a general class of models and to define an intrinsic model of the lambda calculus.

The author presents an interesting semantic study of the system of variable types and brings out an original clean refinement of Scott domains. (The relation of the system and its semantics to other systems and to Scott domains, constructed from the notion of an information system, is discussed in the appendices.) The concept of qualitative domains enables a theoretically clean formulation of the theoretic foundations for variable types, which themselves occur frequently in the context of the study of modern progamming language semantics.