×

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).

MSC:

03G30 Categorical logic, topoi
18B25 Topoi
68Q55 Semantics in the theory of computing
03F35 Second- and higher-order arithmetic and fragments

Citations:

Zbl 0667.00009