L'étude des isomorphismes de types, si l'on autorise les types variants ou les types récursifs, constitue une problématique extrêmement complexe, et on est très loin d'en avoir obtenu une caractérisation complète.
Cependant, si on s'intéresse à des langages orientés objets, comme Java, il est possible d'en coder les interface dans un langage de types restreint à la flèche, le produit et la récursion, et dans ce cadre l'associativité et la commutativité du produit suffisent déjà pour décrire des équivalences intéressantes en pratique pour effectuer des recherche de composants dans des librairies objets.
Dans cet exposé, nous allons prouver que le sous-typage de type récursifs en présence de l'associativité et la commutativité du produit est décidable, en donnant un algorithme de décision polynomial très efficace en pratique. Nous montrerons aussi comment adapter l'algorithme pour qu'il construise aussi les coercions.