Galois transformers and modular abstract interpreters: reusable metatheory for program analysis