Vers la formalisation en Coq des transformateurs de monades modulaires

Abstract

Nous étudions la vérification formelle de programmes avec effets de bord en utilisant un langage purement fonctionnel. Dans le cadre de cette étude, nous avons développé Monae, une librairie Coq qui propose une formalisation des monades et de leurs lois algébriques. Les preuves se font par raisonnement équationnel en utilisant les capacités de réécriture de Coq. Les programmes n'utilisent généralement 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 intéressant de définir de manière canonique les opérations algébriques des monades et leurs primitives lift. Dans cet article, nous présentons l'implémentation des transfor-mateurs de monades modulaires et les preuves des théorèmes qui en découlent en Coq. Nous montrons également leurs utilisations comparées aux transformateurs de monades classiques.