Dans le domaine de l'ingénierie du logiciel, les systèmes de types sont souvent considérés pour la prévention de l'occurrence de termes dénués de sens par rapport à une spécification des types. Dans le cadre de l'extension d'un langage de programmation avec des caractéristiques dédiées, le typage de ces dernières doit être compatible avec les caractéristiques du langage hôte. Cette thèse se situe dans le contexte de la réécriture de termes embarquée dans la programmation orientée objet. Elle vise à développer un système de types avec sous-typage pour le support du filtrage de motifs associatif sur des termes algébriques construits sur des opérateurs variadiques. Ce travail s'appuie sur le langage de réécriture Tom qui fournit des constructions de filtrage de motifs et des stratégies de réécriture à des langages généralistes comme Java. Nous décrivons l'évaluation de code Tom à travers la définition de la sémantique opérationnelle de ce langage en tant qu'élément essentiel de la preuve de la sûreté du système de types. Celui-ci inclut la vérification de types ainsi que l'inférence de types à base de contraintes. Le langage de contraintes est composé d'une part, de contraintes d'égalité, résolues par unification, d'autre part, de contraintes de sous-typage, résolues par la combinaison de phases de simplification, de génération d'une solution et de ramassage de miettes. Le système de types a été intégré au langage Tom, ce qui permet une plus forte expressivité et plus de sûreté a fin d'assurer que les transformations décrites par des règles de réécriture préservent le type des termes.

Dans le domaine de l'ingénierie du logiciel, les systèmes de types sont souvent considérés pour la prévention de l'occurrence de termes dénués de sens par rapport à une spécification des types. Dans le cadre de l'extension d'un langage de programmation avec des caractéristiques dédiées, le typage de ces dernières doit être compatible avec les caractéristiques du langage hôte. Cette thèse se situe dans le contexte de la réécriture de termes embarquée dans la programmation orientée objet. Elle vise à développer un système de types avec sous-typage pour le support du filtrage de motifs associatif sur des termes algébriques construits sur des opérateurs variadiques. Ce travail s'appuie sur le langage de réécriture Tom qui fournit des constructions de filtrage de motifs et des stratégies de réécriture à des langages généralistes comme Java. Nous décrivons l'évaluation de code Tom à travers la définition de la sémantique opérationnelle de ce langage en tant qu'élément essentiel de la preuve de la sûreté du système de types. Celui-ci inclut la vérification de types ainsi que l'inférence de types à base de contraintes. Le langage de contraintes est composé d'une part, de contraintes d'égalité, résolues par unification, d'autre part, de contraintes de sous-typage, résolues par la combinaison de phases de simplification, de génération d'une solution et de ramassage de miettes. Le système de types a été intégré au langage Tom, ce qui permet une plus forte expressivité et plus de sûreté a fin d'assurer que les transformations décrites par des règles de réécriture préservent le type des termes / In software engineering, type systems are often considered in order to prevent the occurrence of meaningless terms in regard to a type specification. When extending a given programming language with new dedicated features, the typing of these features must be compatible with the ones in the host language. This thesis is situated in the context of term rewriting embedded in object-oriented programming and aims to develop a safe type system featuring subtyping for the support of associative pattern matching on algebraic terms built from variadic operators. In this work we consider the Tom rewriting language that provides associative pattern matching constructs and rewrite strategies for Java. We describe Tom code evaluation through the definition of the operational semantics of the Tom language as an essential element to show that the type system is safe. The type system includes type checking and constraint-based type inference. The constraint language is composed of equality constraints solved by unification and subtyping constraints solved by a combination of simplification, generation of solution and garbage collecting. The type system was integrated in Tom which provides both stronger expressiveness and more safety able to ensure that the transformations described by rewrite rules preserve the type of terms

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.