Modular Monadic Meta-Theory

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.