Vers la formalisation en Coq des transformateurs de monades modulaires
In: Actes JFLA 2020 ; Trente-et-unièmes Journées Francophones des Langages Applicatifs (JFLA 2020) ; https://hal.archives-ouvertes.fr/hal-02434736 ; Trente-et-unièmes Journées Francophones des Langages Applicatifs (JFLA 2020), Jan 2020, Gruissan, France. pp.23-30, 2020
Online
Konferenz
Zugriff:
International audience ; 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.
Titel: |
Vers la formalisation en Coq des transformateurs de monades modulaires
|
---|---|
Autor/in / Beteiligte Person: | Sauvage, Célestine ; Affeldt, Reynald ; Nowak, David ; Extra Small Extra Safe (2XS) ; Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL) ; Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS)-Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS) ; National Institute of Advanced Industrial Science and Technology (AIST) |
Link: | |
Zeitschrift: | Actes JFLA 2020 ; Trente-et-unièmes Journées Francophones des Langages Applicatifs (JFLA 2020) ; https://hal.archives-ouvertes.fr/hal-02434736 ; Trente-et-unièmes Journées Francophones des Langages Applicatifs (JFLA 2020), Jan 2020, Gruissan, France. pp.23-30, 2020 |
Veröffentlichung: | HAL CCSD, 2020 |
Medientyp: | Konferenz |
Schlagwort: |
|
Sonstiges: |
|