Retractions of dI-domains as a model for Type:Type. (English) Zbl 0728.68036

Summary: We introduce an extension, with the Type: Type assumption, for a higher- order functional language: in the framework of \(\lambda\beta\) p (the extension of the type-free lambda calculus introduced in R. Amadio and G. Longo (1986b, in “IFIP Conference ‘Formal description of programming concepts’, Ebberup (DK), August 1986”)). Then, we find (using the stable functions and Berry’s dI-domains) a model for \(\lambda\beta\) p. This settles the consistency problem for \(\lambda\beta\) p, up to now open, and gives very simple mathematical models for higher- order calculi with Type:Type. Such models are based on the relevant property that the range of a stable retraction on a dI-domain is still a dI-domain. Finally, we give the categorical description of the models of \(\lambda\beta\) p, based on Moggi-Asperti’s notion of internalization in A. Asperti [Models of higher order calculi internal categories, Carnegie-Mellon report (1988) (in preparation].


68N15 Theory of programming languages
03B15 Higher-order logic; type theory (MSC2010)
Full Text: DOI


[1] Amadio, R.; Bruce, K.; Longo, G., The finitary projections model and the solution of higher order domain equations, (IEEE Symposium on Logic in Computer Science. IEEE Symposium on Logic in Computer Science, Boston, June 1986 (1986))
[2] Amadio, R.; Longo, G., Type-free compiling of parametric types, (IFIP Conference ‘Formal Description of Programming Concepts’. IFIP Conference ‘Formal Description of Programming Concepts’, Ebberup (DK), August 1986 (1986), North-Holland: North-Holland Amsterdam)
[3] Asperti, A., Models of Higher Order Calculi as Internal Categories (1988), Carnegie-Mellon report, in preparation
[4] Asperti, A.; Longo, G., Categories for denotational semantics (1989), in preparation
[5] Barendregt, H. P., (The Lambda Calculus: Its Syntax and Semantic (1984), North-Holland: North-Holland Amsterdam), 491-492, Revised edition · Zbl 0551.03007
[6] Berry, G., Stable models of typed lambda calculi, (Fifth International Colloquium on Automata, Languages and Programs. Fifth International Colloquium on Automata, Languages and Programs, Lecture Notes in Computer Science, Vol. 62 (1978), Springer-Verlag: Springer-Verlag Berlin), 72-89 · Zbl 0382.68041
[7] Burstall, R. M.; Lampson, B., A kernel language for abstract fata types and modules, (Kahn; MacQueen; Plotkin, Symposium on Semantic of Data Types. Symposium on Semantic of Data Types, LNCS, Vol. 173 (1984), Springer-Verlag: Springer-Verlag Berlin) · Zbl 0552.68009
[8] Cardelli, L., A polymorphic lambda-calculus with Type:Type (1986), Syst. Res. Center, Dig. Equip. Corp, preprint
[9] Coquand, T.; Gunter, C.; Winskel, G., dI-Domains as a model of polymorphism, (Proceeding, Third Workshop on the Mathematical Foundations of Programming Language Semantics. Proceeding, Third Workshop on the Mathematical Foundations of Programming Language Semantics, New Orleans, LA (1987)) · Zbl 0644.68041
[10] Girard, J. Y., The system \(F\) of variable types, fifteen years later, Theoret. Comput. Sci., 45 (1986) · Zbl 0623.03013
[11] McCracken, N., An Investigation of a Programming Language with a Polymorphic Type Structure, (Ph.D. thesis (1979), Syracuse University)
[12] Scott, D., A space of retracts (1980), manuscript
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.