Je présenterai plusieurs preuves de normalisation du lambda-calcul simplement typé avec une majoration de la longueur d'une normalisation d'un terme typé donné. J'expliquerai rapidement comment le dernier résultat se généralise au lambda-mu-calcul simplement typé. L'exposé est accessible à tous les membres de l'équipe.