Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Learn how to formalize monadic equational reasoning in dependent-type theory through this 24-minute conference presentation from ICFP 2025. Discover a practical approach to performing equational reasoning about computational effects using monads in the Coq proof assistant, addressing the challenge that while equational reasoning for effectful programs is desirable, it remains difficult to maintain proofs for large examples. Explore how researchers from AIST Japan and Nagoya University formalize a hierarchy of effects using monads by treating the hierarchy of effects and algebraic laws as interfaces, similar to formalizing algebra hierarchies in dependent-type theory. Understand how this approach separates equational laws from models, enabling the use of Coq's sophisticated rewriting capabilities and the construction of lemma libraries for concise program proofs. Examine the formalization of a rich hierarchy of effects including nondeterminism, state, and probability, while seeing mechanized examples of monadic equational reasoning from existing literature. Learn about the application of this framework to designing equational laws for a subset of ML with references, and discover how the resulting framework leverages Coq's mathematical theories to formalize monad models.
