Meta-theory a la carte

Formalizing meta-theory, or proofs about programming languages, in a proof assistant has many well-known benefits. Unfortunately, the considerable effort involved in mechanizing proofs has pre-vented it from becoming standard practice. This cost can be amor-tized by reusing as much of existing mechanized formalizations as possible when building a new language or extending an existing one. One important challenge in achieving reuse is that the induc-tive definitions and proofs used in these formalizations are closed to extension. This forces language designers to cut and paste ex-isting definitions and proofs in an ad-hoc manner and to expend considerable effort to patch up the results. The key contribution of this paper is the development of an in-duction technique for extensible Church encodings using a novel reinterpretation of the universal property of folds. These encodings provide the foundation for a framework, formalized in Coq, which uses type classes to automate the composition of proofs from mod-ular components. This framework enables a more structured ap-proach to the reuse of meta-theory formalizations through the com-position of modular inductive definitions and proofs. Several interesting language features, including binders and general recursion, 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. Bounded induction enables proofs of properties for non-inductive semantic functions, and mediating type classes enable proof adap-tation for more feature-rich languages