GMETA: A Generic Formal Metatheory Framework for First-Order Representations

This paper presents GMETA: a generic framework for first-order representations of variable binding that provides once and for all many of the so-called infrastructure lemmas and definitions required in mechanizations of formal metatheory. The key idea is to employ datatype-generic programming (DGP) and modular programming techniques to deal with the infrastructure overhead. Using a generic universe for representing a large family of object languages we define datatype-generic libraries of infrastructure for first-order representations such as locally nameless or de Bruijn indices. Modules are used to provide templates: a convenient interface between the datatype-generic libraries and the end-users of GMeta. We conducted case studies based on the POPLmark challenge, and showed that dealing with challenging binding constructs, like the ones found in System F<:, is possible with GMeta. All of GMETA's generic infrastructure is implemented in the Coq theorem prover. Furthermore, due to GMETA's modular design, the libraries can be easily used, extended, and customized by users.