Vers la formalisation en Coq des transformateurs de monades modulaires

Nous etudions la verification formelle de programmes avec effets de bord en utilisant un langage purement fonctionnel. Dans le cadre de cette etude, nous avons developpe Monae, une librairie Coq qui propose une formalisation des monades et de leurs lois algebriques. Les preuves se font par raisonnement equationnel en utilisant les capacites de reecriture de Coq. Les programmes n'utilisent generalement pas un seul type d'effet de bord, mais une combinaison de plusieurs d'entre eux. On utilise les transformateurs de monades dans ce but. Cependant, l'approche traditionnelle pour le lifting des primitives n'est pas modulaire. Il est interessant de definir de maniere canonique les operations algebriques des monades et leurs primitives lift. Dans cet article, nous presentons l'implementation des transfor-mateurs de monades modulaires et les preuves des theoremes qui en decoulent en Coq. Nous montrons egalement leurs utilisations comparees aux transformateurs de monades classiques.