The Coq mailing list

[Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>]

David Nowak writes:
 > 
 > More generally are there development in Coq using monad to deal with 
 > side effects?

The  Why  tool   (http://why.lri.fr/)  is  a  verification  conditions
generator.  It  is using  interpretations  in  type theory  internally
(which can be checked by Coq) and they make use of monads to interpret
side-effects, including exceptions.

I've also heard that people  in Sophia-Antipolis using Coq to verify a
C compiler are using monads in Coq.

Hope this helps,
-- 
Jean-Christophe Filliâtre