Abstract FR:

Le systeme f de girard est un lambda-calcul type qui permet de representer toutes les fonctions prouvablement totales dans l'arithmetique de peano du second ordre. Tous les termes typables dans ce systeme sont fortement normalisables, mais il existe des termes normalisables qui ne sont pas typables. Le probleme de l'existence d'une caracterisation recursive de l'ensemble des lambda-termes typables dans ce systeme est toujours ouvert. Nous definissons ici un ensemble de lambda-termes, sl, pour lequel la typabilite est decidable. Il est un sous-ensemble d'une classe s de termes que nous appelons termes simples. Les causes de non typabilite etant liees a des proprietes de normalisation, nous donnons alors une caracterisation syntaxique de normalisation pour certains sous-ensembles de s. Les resultats obtenus precedemment sont generalises et permettent de construire de nouveaux exemples de termes simples normalisables et non-typables