A Generic Formal Metatheory Framework for First-Order Representations

GMeta is 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 mechanization of formal metatheory. The framework employs datatype-generic programming and modular programming techniques to provide a universe representing a family of datatypes. This universe is generic in two different ways:

Using this universe, several libraries providing generic infrastructure lemmas and definitions are implemented. These libraries are then used in case studies based on the POPLmark challenge, showing that dealing with challenging binding constructs, like the ones found in System System F with subtyping (F<:), is possible with GMeta. All of GMeta's generic infrastructure is implemented in Coq, ensuring the soundness of the generic infrastructure. Furthermore, due to GMeta's modular design, the libraries can be easily used, extended and customized by end users.

GMeta Library

The figure below shows an overview of the modular structure of GMeta. The structure is hierarchical, with the more general modules at the top and the more specific modules at the bottom:

Library Overview

Library Codes

DGP Layer DGP_Core Source HTML
LNameless_Meta Source HTML
LNameless_Meta_Env Source HTML
deBruijn_Meta Source HTML
deBruijn_Meta_Env Source HTML
LNameless_Isomorphism Source HTML
deBruijn_Isomorphism Source HTML
LN_Template Source HTML
LN_Template_One_Sort Source HTML
LN_Template_Two_Sort Source HTML
dB_Template Source HTML
dB_Template_Two_Sort Source HTML

Isomorphism Generator



There is a "" file in the directory. To build the generator simple execute that file:
> ./
Now you should have a "genIsos" executable in your directory.

You have two options for using the tool:
  1. Either copy it to the main directory of your coq development
  2. Put genIsos somewhere in your PATH



Here we give an explanation how to formalize the metatheory of the simply typed lambda calculus (STLC) using GMeta. The formalization can be done in four steps.

  1. Defining Syntax: The first step is to define the syntax for the object language that is going to be formalized, using one of the first-order representations supported by GMeta.
    • In case of STLC, the sets of pseudo-types and pseudo-terms should be defined by the user. Cf. 1. step in Syntax or in Isomorphism.
  2. Defining isomorphisms for interfacing with GMeta: The second step is to provide annotations to guide the isomorphism generation tool to produce the isomorphism modules automatically. Cf. 1. and 2. step in Syntax.
    • The isomorphisms can be created manually. Cf. 2. step in Isomorphism.
  3. Importing the infrastructure: After having generated the isomorphism modules, we can use them to instantiate some of GMeta infrastructure templates, and import these to obtain the desired infrastructure lemmas and definitions.
    • In case of STLC, if the user chooses to use the locally nameless approach for the formalization, the template in LN_Template.v can be used. Cf. 3. step in Formalization.
  4. Metatheory formalization: Now the user can proceed with the formalization using the imported infrastructure.

Formalization of STLC using the locally nameless approach

STLC Syntax Source HTML
Isomorphism Source HTML
Formalization Source HTML

Case Studies

In order to verify the effectiveness of GMeta in reducing the infrastructure overhead, we conducted case studies using locally nameless and de Bruijn representations.


GMeta can reduce the infrastructure overhead because it provides reuse of boilerplate definitions and lemmas. By boilerplate we mean the following:


For each case study, GMeta was employed in two different ways, according to how much the user needs to know about GMeta and DGP in order to successfully achieve reuse:


The case studies measure the number of definitions and lemmas that have been saved (both the total number and the number of boilerplate definitions and lemmas). The results are shown below and presented in terms of the percentage of definitions and lemmas saved.

Case studies using locally nameless approach

STLC Isomorphism* Source HTML
Basic Definitions Source HTML
Infrastructure Source HTML
Soundness Source HTML
System F<: Isomorphism* Source HTML
Basic Definitions Source HTML
Infrastructure Source HTML
Soundness Source HTML
Advanced Definitions Source HTML
Infrastructure Source HTML
Soundness Source HTML

Case studies using de Bruijn indices

System F<: Isomorphism Source HTML
Basic Main Source HTML

* Isomorphism can be generated automatically.


The whole libraries including case studies can be downloaded from here. Note that the libraries are implemented using the Coq version 8.2pl1. We are going to update the libraries to the new Coq versions. (Uncompress the tar file and use "make" to compile the whole library. )

GMeta 2

We also have a experimental and incomplete version (both in Agda and in Coq) of GMeta that uses a more expressive universe based on:

Morris, P. and Thorsten Altenkirch and Conor McBride, Exploring the regular tree types, In Types for Proofs and Programs, 2004

The main purpose is just to illustrate that more expressive universes are essentially orthogonal to the main ideas of GMeta. You can find the Agda version here and the Coq version here.



What is GMeta?
GMeta Library
Iso Generator
Case Studies
GMeta 2 (Experimental)