Formalization of monadic equational reasoning a la Ssreflect/MathComp
- 講者Takafumi Saikawa 先生 (M. Math. Sc., Nagoya University and Peano System Inc.)
邀請人：穆信成 - 時間2019-07-19 (Fri.) 14:00 ~ 17:00
- 地點資訊所新館107演講廳
摘要
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".