  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 first-class type constructors, first-class
polymorphism, or type quantification; instead, we rely on a domain-theoretic
model of the type system in a universal domain to provide these features.
  These ideas are implemented in the Tycon library for the Isabelle theorem
prover, which builds on the HOLCF library of domain theory. The Tycon library
provides various axiomatic type constructor classes, including functors and
monads. It also provides automation for instantiating those classes, and for
defining further subclasses.
  We use the Tycon library to formalize three Haskell monad transformers: the
error transformer, the writer transformer, and the resumption transformer. The
error and writer transformers do not universally preserve the monad laws;
however, we establish datatype invariants for each, showing that they are valid
monads when viewed as abstract datatypes.
