Effective Reasoning about Effectful Programs

Jeremy Gibbons ( Oxford University Computing Laboratory )

I will talk about the use of monads and idioms (aka "applicative functors", or "strong lax-monoidal functors") for structuring pure functional programs with computational effects; in particular, I will discuss reasoning principles for such effectful programs. I was intending to present an elegant theorem about inverting effectful programs, but sadly it is still a conjecture in pieces on the floor - so instead, I will hope that you can help to show me the way forward. (This is joint work with Richard Bird.)