Avec mon ancien directeur de thèse Pierre Valarcher, professeur à l'Université Paris-Est Créteil, nous avons travaillé sur la caractérisation impérative des algorithmes en temps polynomial c'est à dire sur la preuve que d'une part notre langage de programmation impératif PLoopC est bien en temps polynomial, et d'autre part que tout algorithme séquentiel peut être simulé par PLoopC.

Pour faire cette preuve nous avons utilisé les ASMs, c'est à dire une présentation impérative des algorithmes, mais d'autres modèles ont été présentés dans un cadre fonctionnel, comme les récurseurs de Moschovakis. De plus, de nombreux langages (comme le langage LPL de Patrick Baillot, Marco Gaboardi et Virgile Mogbil) essayant de caractériser les algorithmes polynomiaux sont des langages fonctionnels.

Notre but est donc de créer une version fonctionnelle de notre langage, et de prouver l'équivalence algorithmique entre la version impérative et la version fonctionnelle, ce qui permettra ensuite de comparer la version fonctionnelle aux modèles et langages existants.