Un ensemble des mes travaux porte sur la théorie équationnelle de la jointure (naturelle) et de la réunion (interne) de relations (tables d'une base de données relationnelle). Ces deux opérations s’avèrent être le meet et join dans une classe de treillis, les treillis relationnels. Nous proposons une axiomatisation de ces opérations, envisageant des possibles retombés dans l'optimisation des requêtes dans des langages type SQL. Dans deux articles nous démontrons que le problème de plonger un treillis finis dans un treillis relationnel est indécidable ; une conséquence de ce résultat est que la théorie quasi-équationnelle de ces treillis est indécidable et qu’il existe une formule de Horn vraie dans tous le treillis relationnels finis mais réfutée par un de ces treillis infinis. Notre travail répond à des nombreuses question posés dans (Litak et al., 2015). Finalement, dans notre travail le plus recent, nous donnons une contribution déterminante à ce sujet, en montrant que la théorie équationnelle de ces treillis est décidable. C’est-à-dire, nous donnons une procédure de décision pour déterminer su deux requêtes construites à partir de la jointure naturelle et de la réunion interne donnent toujours le même résultat. Notre résultat ouvre la porte à des nouvelles recherche, par exemple autour de la complexité de ce problème de décision.

Nous avons étudié l'élimination des point fixes dans la logique intuitionniste en proposant un algorithme pour calculer une formule intuitionniste équivalente à une formule intuitionniste avec des points fixes, et des bornes supérieures au nombre d'itérations de Kleene nécessaires à calculer le points fixe d'une formule. Cet travail a été récemment développé ultérieurement et une version longue est à présent soumise au journal TOCL. Ce travail est partie d'un programme général visant à identifier des principes uniformes qui sont cause de l'écroulement des hiérarchies d'alternance de points fixes dans les mu-calculs. La collaboration avec Gouveia autour des logiques avec points fixes a ensuite abouti à notre production la plus récente. Nous considérons le mu-calcul propositionnel modale, c’est-à-dire la logique modale proportionnelle K étendue avec des opérateurs de point fixe. On dit qu’une formule de cette logique a un ordinal de clôture si elle converge---uniformément, dans tout modèle---à son plus petit point-fixe avec alpha itérations (alpha est ici un ordinal); les logiciens de Varsovie ont posé la question de caractériser les ordinaux de clôture. Il était connu que tout ordinal plus petit que omega² est un tel ordinal. Nous montrons que Omega (le plus petit ordinal non dénombrable) est aussi un tel ordinal, et que les ordinaux de clôture sont fermés par rapport à la somme ordinale. Notre travail passe par la caractérisation du fragment aleph₁-continu (que nous montrons être décidable) de cette logique et éclaircit comment les ordinaux de clôture peuvent se construire à partir de petits cardinaux infinis (aleph₀, aleph₁).

Cet axe de recherche a été développée principalement en collaboration avec Fred Wehrung, du LMNO. L'objectif au début de notre collaboration était de caractériser la théorie équationnelle de treillis dont les éléments ont nature combinatoire, les Permutohèdres et les Associahèdres. Après quatre années de recherche, l’objectif a été atteint : nous avons démontré que les treillis de permutations (c-à-d. les Permutohèdres) satisfont des équations non-triviales dans la signature des treillis  ; de plus, leur théorie équationnelle est décidable. Nous avons soumis cet excellent résultat à un journal très sélectif, le « Journal of the European Mathematical Society ». La collaboration avec Wehrung a été très productive et a aussi donné naissance à deux chapitres (dont un en collaboration avec Nathalie Caspard du LACL) d’une monographie est déshormais une référence majeure de notre domaine. Une axe de recherche proche, autour d’une version continue de l’ordre faible de Bruhat, est à présent développée en collaboration avec M. J. Gouveia de l’Université de Lisbonne.

Cette recherche prolonge mes travaux sur les mu-treillis dont les retombés envisagées se situent dans la théorie et la pratique des langages de programmation. Obtenir ces retombés comporte se dérouter des ensembles ordonnés vers les catégories  : les flèches d'une catégorie modélisent les programmes et donnent un sens à la notion d'équivalence entre programmes. Les catégories mu-bicomplètes étudiées sont définies par la propriété de posséder les produits et coproduits finis, et les algèbres initiales et les coalgèbres finales des foncteurs définissables par les mu-termes. Un problème ouvert depuis 2002 était de trouver une syntaxe, qui généralise la syntaxe des preuves circulaire, mais qui soit aussi complète au regard de la notion de catégorie mu-bicomplète libre. Garder l'aspect circulaire des preuves est une condition sine-qua-non  : sur la circularité repose la possibilité de comprendre par une seule théorie styles de programmation opposés, fonctionnel et impératif. Les travaux de thèse de J. Fortier répondent au problème de 2002. Nous avons décrit la nouvelle syntaxe, incluant une règle explicite de coupure  ; la syntaxe est complète  ; nous prouvons la correction forte du système et illustrons un processus d'élimination de coupures qui construit, à partir d'une preuve circulaire finie avec coupures, un arbre de preuve sans coupures infini (il peut avoir des branches infinies). Parmi les conséquences plus fortes, une caractérisation (via le processus d'élimination des coupures) des fonctions définissables par la notion de catégorie mu-bicomplète ; du coté des langages de programmation, nos travaux amènent à des systèmes de typage statique (incomplets) assurant la terminaison des programmes fonctionnels utilisant la récursion (et/ou la corécursion).