Institute of Information Science Academia Sinica
Topic: Formalization of monadic equational reasoning a la Ssreflect/MathComp
Speaker: Mr. Takafumi Saikawa (M. Math. Sc., Nagoya University and Peano System Inc.)
Date: 2019-07-19 (Fri) 14:00 – 17:00
Location: Auditorium107 at IIS new Building
Host: Shin-Cheng Mu

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.

The draft is here:https://staff.aist.go.jp/reynald.affeldt/documents/monae.pdf

[1] Jeremy Gibbons and Ralf Hinze, "Just do It: Simple Monadic Equational Reasoning".

 http://www.cs.ox.ac.uk/jeremy.gibbons/publications/mr.pdf