A domain-theoretic model construction for Coquand/Huet's calcu-lus of constructions

The Calculus of Constructions is one of the most powerful systems of constructive logic. It consists of three logical levels: proofs, propo-sitions, kinds. The kinds are the types of operations, i.e., construc-tions of propositions. Both, the level of propositions and the level of kinds, are closed under general rules of quantification. A model construction involves giving meaning to the objects of each of the three levels in such a way that the quantification rules are satisfied. The aim is to give a construction that uses ordered structures, known as domains. In the present work domain constructions used for the interpretation of the quantification constructs are presented in a general way and computability issues are discussed.