The system \({\mathcal F}\) of variable types, fifteen years later (Q1091379)

The paper concentrates on the construction of a suitable semantics for the system F of variable types, i.e. schemes of abstraction with respect to types. The main problem in finding interpretation of terms of variable types is connected with generally unrestrained formation of type abstraction and the schema of evaluation of functions of universal type. Since its formulation in the system F, the idea of variable types has become a common idea in computer science. However, there has not been much progress in the underlying theory. The author develops a semantics based on the category-theoretic notion of direct limit, allowing to describe the behaviour of a variable type of any domain by its behaviour on finite domains only. To do so, an original construction is introduced, viz. the qualitative domains, which present a refinement of Scott domains. The interpretation obtained is demonstrated on simple examples, a small universal model (''the intrinsic model'') of lambda calculus is defined, and the concept of totality is discussed.