Terminaison basée sur les types et filtrage dépendant pour le calcul des constructions inductives

Proof assistants based on dependent type theory are gaining adoption as a tool to develop certified programs. A successful example is the Coq proof assistant, an implementation of a dependent type theory called the Calculus of Inductive Constructions (CIC). Coq is a functional programming language with an expressive type system that allows to specify and prove properties of programs in a higher-order predicate logic. Motivated by the success of Coq and the desire of improving its usability, in this thesis we study some limitations of current implementations of Coq and its underlying theory, CIC. We propose two extension of CIC that partially overcome these limitations and serve as a theoretical basis for future implementations of Coq. First, we study the problem of termination of recursive functions. In Coq, all recursive functions must be terminating, in order to ensure the consistency of the underlying logic. Current techniques for checking termination are based on syntactical criteria and their limitations appear often in practice. We propose an extension of CIC using a type-based mechanism for ensuring termination of recursive functions. Our main contribution is a proof of Strong Normalization and Logical Consistency for this extension. Second, we study pattern-matching definitions in CIC. With dependent types it is possible to write more precise and safer definitions by pattern matching than with traditional functional programming languages such as Haskell and ML. Based on the success of dependently-typed programming languages such as Epigram and Agda, we develop an extension of CIC with similar features.Les assistants de preuve basés sur des théories des types dépendants sont de plus en plus utilisé comme un outil pour développer programmes certifiés. Un exemple réussi est l'assistant de preuves Coq, fondé sur le Calcul des Constructions Inductives (CCI). Coq est un langage de programmation fonctionnel dont un expressif système de type qui permet de préciser et de démontrer des propriétés des programmes dans une logique d'ordre supérieur. Motivé par le succès de Coq et le désir d'améliorer sa facilité d'utilisation, dans cette thèse nous étudions certaines limitations des implémentations actuelles de Coq et sa théorie sous-jacente, CCI. Nous proposons deux extension de CCI que partiellement resourdre ces limitations et que on peut utiliser pour des futures implémentations de Coq. Nous étudions le problème de la terminaison des fonctions récursives. En Coq, la terminaison des fonctions récursives assure la cohérence de la logique sous-jacente. Les techniques actuelles assurant la terminaison de fonctions récursives sont fondées sur des critères syntaxiques et leurs limitations apparaissent souvent dans la pratique. Nous proposons une extension de CCI en utilisant un mécanisme basé sur les type pour assurer la terminaison des fonctions récursives. Notre principale contribution est une preuve de la normalisation forte et la cohérence logique de cette extension. Nous étudions les définitions par filtrage dans le CCI. Avec des types dépendants, il est possible d'écrire des définitions par filtrage plus précises, par rapport à des langages de programmation fonctionnels Haskell et ML. Basé sur le succès des langages de programmation avec types dépendants, comme Epigram et Agda, nous développons une extension du CCI avec des fonctions similaires