Nous nous intéresserons à un système de types permettant de garantir qu'un lambda-terme est exécutable en temps polynomial. L'approche considérée sera celle de la logique linéaire light (Girard, 1995), un système dont l'élimination des coupures est polynomiale. Plus précisément nous utiliserons la variante affine (light affine logic, LAL) proposée par Asperti. Si un lambda-terme est bien typé dans ce système et prend comme argument mettons un entier binaire, alors il admet une borne polynomiale pour son exécution sur toute entrée.
Nous introduirons une relation de sous-typage naturelle permettant de généraliser l'assignation de type dans LAL, puis montrerons la décidabilité du problème de la typabilité (dans le système sans polymorphisme), notre résultat principal. Pour cela nous ramènerons le problème à la résolution de systèmes d'inéquations sur les mots sur un alphabet binaire.