The Coq Proof Assistant

Stephanie Weirich and Brian Aydemir are pleased to announce LNgen, a prototype tool for generating Coq code for the infrastructure associated with a locally nameless representation. This work builds upon their work with Charguéraud, Pierce, and Pollack on Engineering Formal Metatheory, where they described a locally nameless strategy for representing languages with binding.

LNgen uses a subset of the Ott specification language as its input language. Currently, it supports the definition of syntax with single binders. Compared to the recently announced locally nameless backend for Ott, LNgen does not handle the definition of relations, but it does generate a large collection of "infrastructure" lemmas and their proofs, e.g., facts about substitution.