Extraction de programmes dans le Calcul des Constructions

This thesis introduces an extension of the Calculus of Constructions of Coquand and Huet which allows the extraction of certified programs from constructive proofs. A modified realisability notion is introduced and its properties are studied. An impredicative encoding of a large class of inductive definitions is proposed.Cette thèse propose une extension du Calcul des Constructions de Coquand et Huet qui permet l'extraction de programmes certifiés à partir de preuve constructive. Une notion de réalisabilité modifiée est introduite et étudiée. Un codage imprédicatif d'une large classe de définitions inductives est proposé