Abstract FR:

L'objet de cette these est la meta-theorie du calcul des constructions inductives, c'est a dire les calcul des constructions etendu par des types et des predicats inductifs. Le calcul des constructions a ete presente en 1985 par thierry coquand. Il s'agit d'un lambda-calcul type qui, a travers l'isomorphisme dit de curry-howard, peut-etre vu comme un formalisme logique. Ce systeme est particulierement expressif du point de vue algorithmique et peut facilement etre mis en uvre sur ordinateur. L'ajout de types inductifs primitifs permet une meilleure representation des types de donnees que dans le calcul originel. Le resultat essentiel est que le systeme verifie bien la propriete de normalisation forte. On en deduit la coherence logique, la confluence et la decidabilite du typage. L'aspect le plus spectaculaire de l'extension par des types inductifs est la possibilite de definir de nouveaux types et de nouvelles propositions par recurrence structurelle (elimination forte). L'interpretation de l'elimination forte dans une preuve de normalisation par reductibilite est la nouveaute essentielle de ce travail. De plus, nous considerons ici un systeme avec eta-conversion. Nous montrons qu'alors la propriete de confluence n'est plus combinatoire mais depend de la normalisation.