This paper presents 3MT, a framework for developing modular
mechanized meta-theory of languages with effects. Using 3MT,
individual language features and their corresponding definitions --
semantic functions, theorem statements and proofs
-- can be built separately and then reused to create different
languages with fully mechanized meta-theory. 3MT tackles the
multi-faceted problem of modularity in this setting by combining
modular datatypes and monads to define effectful
semantic functions on a per-feature basis, without fixing a
particular set of effects or language constructs.

The main challenge that 3MT addresses is how to modularize the theorems
and proofs for these modular monadic definitions.
Theorem statements like type soundness depend intimately on the
effects used in a language, making modularity particularly
challenging to achieve. 3MT overcomes this problem by splitting theorems into
two parts: a reusable theorem that captures type soundness of a
feature in a language-independent way, and a language-specific type
soundness theorem. Proofs of the first only mention the effects of a
specific feature, and proofs of the second need only know that first
theorem holds for the features included in a language. To establish
both theorems, 3MT uses two key reasoning techniques:
modular induction and algebraic laws about effects. Several effectful
language features, including references and errors, illustrate the
capabilities of our framework. We reuse these features to build fully
mechanized definitions and proofs for a number of languages, including
a version of mini-ML with effects.