Titre :

A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning

Auteur(s) :

Affeldt, Reynald [Auteur]
National Institute of Advanced Industrial Science and Technology [AIST]
Nowak, David [Auteur]
Extra Small Extra Safe [2XS]
Centre National de la Recherche Scientifique [CNRS]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Saikawa, Takafumi [Auteur]

Titre de la manifestation scientifique :

Mathematics of Program Construction - 13th International Conference, MPC 2019, Porto, Portugal, October 7-9, 2019

Ville :

Porto

Pays :

Portugal

Date de début de la manifestation scientifique :

2019-10-07

Titre de l’ouvrage :

Mathematics of Program Construction - 13th International Conference, MPC 2019, Porto, Portugal, October 7-9, 2019

Titre de la revue :

Mathematics of Program Construction - 13th International Conference, MPC 2019, Porto, Portugal, October 7-9, 2019, Proceedings

Date de publication :

2019-10-20

Discipline(s) HAL :

Informatique [cs]/Logique en informatique [cs.LO]

Résumé en anglais : [en]

One can perform equational reasoning about computational effects with a purely functional programming language thanks to monads. Even though equational reasoning for effectful programs is desirable, it is not yet mainstream. ...
Lire la suite >One can perform equational reasoning about computational effects with a purely functional programming language thanks to monads. Even though equational reasoning for effectful programs is desirable, it is not yet mainstream. This is partly because it is difficult to maintain pencil-and-paper proofs of large examples. We propose a formalization of a hierarchy of effects using monads in the Coq proof assistant that makes equational reasoning practical. Our main idea is to formalize the hierarchy of effects and algebraic laws like it is done when formalizing hierarchy of traditional algebras. We can then take advantage of the sophisticated rewriting capabilities of Coq to achieve concise proofs of programs. We also show how to ensure the consistency of our hierarchy by providing rigorous models. We explain the various techniques we use to formalize a rich hierarchy of effects (with nondeterminism, state, probability, and more), to mechanize numerous examples from the literature, and we furthermore discuss extensions and new applications.Lire moins >

Langue :

Anglais

Comité de lecture :

Oui

Audience :

Internationale

Vulgarisation :

Non

Collections :

• Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL