Formal Verification of Monad Transformers

Brian Huffman

We present techniques for reasoning about constructor classes that (like the monad class) fix polymorphic operations and assert polymorphic axioms. We do not require a logic with f…