Cette thèse concerne la combinaison du lambda-calcul et de la réécriture, dont nous étudions principalement deux propriétés : la confluence et la normalisation forte. Nous commençons par étudier sous quelles conditions la combinaison d'une relation de réécriture conditionnelle confluente au lambda-calcul donne une relation de réécriture confluente. Ensuite nous nous intéressons aux preuves de normalisation forte de lambda-calculs typés utilisant la technique de réductibilité. Notre contribution la plus importante est une comparaison de diverses variantes de cette technique, utilisant comme outil de comparaison la manière dont ces variantes s'étendent à la réécriture et dont elles prennent en compte les types unions et les types existentiels implicites. Enfin, nous présentons un critère, basé sur un système de types contraints, pour la normalisation forte de la réécriture conditionnelle combinée au lambda-calcul. Notre approche étend des critères de terminaison existants qui utilisent des annotations de taille. C'est à notre connaissance le premier critère de terminaison pour la réécriture conditionnelle avec membres droits d'ordre supérieur qui prenne en compte, dans l'argument de terminaison, de l'information issue de la satisfaction des conditions des règles de réécriture