Une Théorie des Constructions Inductives
Benjamin Werner · HAL (Le Centre pour la Communication Scientifique Directe) · 1994
This thesis presents the meta-theory of the Calculus of Inductive Constructions, that is the Calculus of Constructions of Coqaund and Huet, extended by inductive types by Coquand and Paulin-Mohring. The main result is storng mormalisation which entails logical consistency and decidability of typing. The system we consider here includes eta-reduction, and thus confuence has to be proved after normalisation. We also show that for typed lambda-calculi, confluence of the beta-eta reduction is a logical and not a combinatorial property.