The system \({\mathcal F}\) of variable types, fifteen years later. (English) Zbl 0623.03013

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.
Reviewer: J.Zlatuska


03B40 Combinatory logic and lambda calculus
18A35 Categories admitting limits (complete categories), functors preserving limits, completions
68Q65 Abstract data types; algebraic specification
Full Text: DOI


[1] Berry, G., Modèles complètement adéquats et stables des λ-calcul typés, (Thèse de Doctorat d’Etat (1979), Université Paris VII)
[2] Coquand, T.; Huet, G., Une théorie des constructions, (Proc. ASL Congress. Proc. ASL Congress, Orsay (1985), North-holland: North-holland Amsterdam), to appear
[3] Girard, J.-Y., Une extension de l’interpretation fonctionnelle de Gödel à l’analyse et son application à l’élimination des coupures dans l’analyse et la théorie des types, (Fenstad, J. F., Proc. 2nd Scandinavian Logic Symp. (1971), North-Holland: North-Holland Amsterdam), 63-92 · Zbl 0221.02013
[4] Girard, J. Y., Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur, (Thèse d’Etat (1972), Université Paris VII)
[5] Girard, J.-Y., Quelques résultats sur les interprétations fonctionnelles, (Mathias; Rogers, Cambridge Summer School in Mathematical Logic. Cambridge Summer School in Mathematical Logic, Lecture Notes in Mathematics, 337 (1973), Springer: Springer Berlin), 232-252 · Zbl 0287.02017
[7] Reynolds, J. C., Polymorphism is not set-theoretic, (Internat. Symp. on Semantics of Data Types. Internat. Symp. on Semantics of Data Types, Lecture Notes in Computer Science, 173 (1984), Springer: Springer Berlin), 145-156 · Zbl 0554.03012
[8] Scott, D., Domains for denotational semantics, (Proc. ICALP’82. Proc. ICALP’82, Aarhus. Proc. ICALP’82. Proc. ICALP’82, Aarhus, Lecture Notes in Computer Science, 140 (1982), Springer: Springer Berlin) · Zbl 0495.68025
[9] Troelstra, A. S., Notes on intuitionistic second order arithmetic, (Mathias; Rogers, Cambridge Summer School in Mathematical Logic. Cambridge Summer School in Mathematical Logic, Lecture Notes in Mathematics, 337 (1973), Springer: Springer Berlin), 171-205 · Zbl 0275.02036
[10] Winskel, G., Events in computation, (Ph.D. Thesis (1981)), Edinburgh
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.