Reasoning with monads

[Roman Garcia]

Hi,

  I'm searching information on reasoning with monads.
  Has anybody made proofs with the IO monads?
  What kind of program transformation is possible with monads?
  Are there new ways to think about monad-based programs?

I'd be very grateful if you could send me any related information.
Thanks in advance. Roman.