Formalization of monadic equational reasoning a la Ssreflect/MathComp
- LecturerMr. Takafumi Saikawa (M. Math. Sc., Nagoya University and Peano System Inc.)
Host: Shin-Cheng Mu - Time2019-07-19 (Fri.) 14:00 ~ 17:00
- LocationAuditorium107 at IIS new Building
Abstract
I am going to talk about a formalization of computational effects according to the monadic equational reasoning by Gibbons and Hinze [1].
In their framework in [1], the effects are expressed as monads extended by effect operators. Haskell's library of MonadFail, MonadState, etc. are based on this, and can be reasoned about by our formal development.
Our formal proofs are written in the proof assistant Coq extending its Ssreflect/MathComp library, which features hierarchical definitions of algebraic theories and heavy uses of equational rewriting. Both of those mechanisms nicely fit to our purpose of defining a hierarchy of monadic theories and reasoning equationally on them.
The talk will begin with an overview of the mechanisms and examples. After that, we will continue into the theoretical background, further examples, and/or the future directions of this work.
【Draft】
[1] Jeremy Gibbons and Ralf Hinze, "Just do It: Simple Monadic Equational Reasoning".