Retractions of dI-domains as a model for Type:Type.

*(English)*Zbl 0728.68036Summary: 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].

##### MSC:

68N15 | Theory of programming languages |

03B15 | Higher-order logic; type theory (MSC2010) |

Full Text:
DOI

##### References:

[1] | Amadio, R.; Bruce, K.; Longo, G., The finitary projections model and the solution of higher order domain equations, () |

[2] | Amadio, R.; Longo, G., Type-free compiling of parametric types, () |

[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., (), 491-492, Revised edition |

[6] | Berry, G., Stable models of typed lambda calculi, (), 72-89 |

[7] | Burstall, R.M.; Lampson, B., A kernel language for abstract fata types and modules, () · 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, () · 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, () |

[12] | Scott, D.; Scott, D.; Scott, D., A space of retracts, (), SIAM J. comput., 5, 522-587, (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. 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.