Title :

A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning

Author(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]

Conference title :

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

City :

Porto

Country :

Portugal

Start date of the conference :

2019-10-07

Book title :

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

Journal title :

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

Publication date :

2019-10-20

HAL domain(s) :

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

English abstract : [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. ...
Show more >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.Show less >

Language :

Anglais

Peer reviewed article :

Oui

Audience :

Internationale

Popular science :

Non

Collections :

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

Source :

Harvested from HAL