  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 monadic equational reasoning practical. Our
main idea is to formalize the hierarchy of effects and algebraic laws as
interfaces like it is done when formalizing hierarchy of algebras in dependent
type theory. Thanks to this approach, we clearly separate equational laws from
models. We can then take advantage of the sophisticated rewriting capabilities
of Coq and build libraries of lemmas to achieve concise proofs of programs. We
can also use the resulting framework to leverage on Coq's mathematical theories
and formalize models of monads. In this article, we explain how we formalize a
rich hierarchy of effects (nondeterminism, state, probability, etc.), how we
mechanize examples of monadic equational reasoning from the literature, and how
we apply our framework to the design of equational laws for a subset of ML with
references.

Logic in Computer Science