Hyland, J. Martin E.; Pitts, Andrew M. The theory of constructions: Categorical semantics and topos-theoretic models. (English) Zbl 0721.03048 Categories in computer science and logic, Proc. AMS-IMS-SIAM Jt. Summer Res. Conf., Boulder/Colo. 1987, Contemp. Math. 92, 137-199 (1989). Summary: [For the entire collection see Zbl 0667.00009.] A syntactically rich version of the Coquand-Huet theory of constructions is described as a theory of dependent types involving expressions at three different levels (terms, types and orders) together with indexed sums and products of various kinds. Two extensions of the theory involving universal types are also discussed. A complete category- theoretic explanation of the meaning of the theory is built up, based upon a careful analysis of the categorical semantics of Martin-Löf’s theory of dependent types. Finally, two particular models of the theory of constructions are described (modelling the two extensions of the theory mentioned above). In these models, the orders and types are denoted by particular kinds of Grothendieck topos, namely algebraic toposes (toposes of presheaves on small categories with finite limits) and algebraic-localic toposes (toposes of presheaves on meet semi- lattices). Cited in 28 Documents MSC: 03G30 Categorical logic, topoi 18B25 Topoi 68Q55 Semantics in the theory of computing 03F35 Second- and higher-order arithmetic and fragments Keywords:Coquand-Huet theory of constructions; universal types; categorical semantics of Martin-Löf’s theory of dependent types; Grothendieck topos; algebraic toposes; algebraic-localic toposes Citations:Zbl 0667.00009 PDFBibTeX XML