zbMATH — the first resource for mathematics

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, Orsay, (1985), 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 Amsterdam), 63-92
[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, Lecture Notes in Mathematics, 337, (1973), Springer Berlin), 232-252 · Zbl 0287.02017
[6] J.Y. Girard, Normal functors, power series and lambda-calculus, Ann. Pure Appl. Logaic, to appear.
[7] Reynolds, J. C., Polymorphism is not set-theoretic, (Internat. Symp. on Semantics of Data Types, Lecture Notes in Computer Science, 173, (1984), Springer Berlin), 145-156 · Zbl 0554.03012
[8] Scott, D., Domains for denotational semantics, (Proc. ICALP’82, Aarhus, Lecture Notes in Computer Science, 140, (1982), Springer Berlin) · Zbl 0495.68025
[9] Troelstra, A. S., Notes on intuitionistic second order arithmetic, (Mathias; Rogers, Cambridge Summer School in Mathematical Logic, Lecture Notes in Mathematics, 337, (1973), 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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.