A Practical Formalization of Monadic Equational Reasoning in Dependent-type Theory

Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

One can perform equational reasoning about computational effects with a purely functional programming language thanks to monads. Even though equational reasoning for effectful prog…