La logique affine light (LAL) ([Girard98, Asperti98]) peut être utilisée comme un système de types pour le lambda-calcul: elle garantit pour un lambda-terme bien typé la proprieté d'être exécutable en temps polynomial. Cependant ce système présente deux inconvenients:

• pour obtenir l'exécution en temps polynomial des termes bien typés il ne suffit pas d'appliquer la beta-reduction au terme pur: il faut utiliser les réseaux de preuves ou le lambda-calcul light ([Terui01]);
• à cause des deux exponentielles('bang' et 'paragraphe') le système de types est complexe.

Nous proposons un nouveau système appelé Logique affine light duale (DLAL) surmontant ces difficultés: DLAL a 2 connecteurs flèche (linéaire et intuitionniste) et l'exponentielle 'paragraphe'. DLAL correspond à un sous-système simple de LAL et offre les propriétés suivantes: garantie de la béta-reduction polynomiale pour les termes DLAL-typés et complétude par rapport aux fonctions PTIME.