Modular Monadic Meta-Theory

Benjamin Delaware, Steven Keuchel, Tom Schrijvers, Bruno C. d. S. Oliveira

abstract

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.

MiniML Features
Names.v     PNames.v Base definitions for the case study.
Arith.v Arithmetic Expressions
Bool.v Boolean Expressions
Lambda.v Function Abstraction and Application
Ref.v References
Exception.v Exceptions
Additional Files
Makefile Makefile to build the framework and case study.
FJ_tactics.v Custom tactics used in the case study.