(travail en collaboration avec Kazushige Terui)
L'étude de la complexité de l'élimination des coupures en Logique Linéaire a permis l'introduction de systèmes logiques caractérisant le calcul en temps déterministe polynomial, comme la Logique Linéaire Light (Girard 1995) ou sa version affine, LAL (Asperti 1998), plus commode en pratique. Ces logiques, en particulier LAL, peuvent ensuite être utilisées comme des systèmes de types pour le lambda-calcul garantissant pour un programme bien typé la propriété d'être exécutable en temps polynomial. Cependant attention, la borne polynomiale n'est pas garantie sur la beta-réduction du lambda-terme lui-même, mais sur son exécution au moyen des réseaux de preuves (ou d'extensions du lambda-calcul comme le lambda-calcul light de Terui). Le réseau de preuve peut de toute façon être obtenu à partir du lambda-terme grâce à la dérivation de type... mais en pratique on préférerait une approche où le certificat de complexité (type) et le programme lui-même (lambda-terme) sont séparés.
Pour remédier à cette difficulté nous proposons un nouveau système (DLAL: Dual Light Affine Logic) correspondant à un fragment de LAL. Ce système a un langage de types simple avec une flèche linéaire, une flèche intuitionniste et une modalité. Sa propriété principale est la suivante: un terme typable dans DLAL est normalisable en temps polynomial par beta-réduction et avec n'importe quelle stratégie. Par ailleurs tout comme LAL, DLAL permet de représenter toutes les fonctions calculables en temps polynomial. Enfin, un dernier avantage de DLAL est qu'il devrait permettre une inférence de type plus efficace.