Meta-theory à la Carte

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

abstract

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 prevented it from becoming standard practice. This cost can be amortized 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 inductive definitions and proofs used in these formalizations are closed to extension. This forces language designers to cut and paste existing 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 induction 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 modular components. This framework enables a more structured approach to the reuse of meta-theory formalizations through the composition 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 adaptation for more feature-rich languages.

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
Mu.v Fixpoint Combinator
Nat_Case.v Case Expression for Natural Numbers
Additional Files
Makefile Makefile to build the framework and case study.
FJ_tactics.v Custom tactics used in the case study.
Composed Language Source Files
    test_A.v Syntax and semantics of simple Arithmetic expression language.
        test_AB.v Syntax and semantics of Boolean and Arithmetic expression language.
        test_AL.v Syntax and semantics of Arithmetic expression language with functions.
        test_BL.v Syntax and semantics of Boolean expression language with functions.
            test_ABL.v Syntax and semantics of Boolean and Arithmetic expression language with functions.
                                    MiniML.v Syntax and semantics for mini-ML.