InfraGen: Binder Boilerplate at Scale [pdf] [bib]

Abstract

A key concern in the mechanization of programming language metatheory is the representation of terms with variable binding. The properties of operations manipulating terms are notoriously burdensome to prove and the amount of work required to scale formalizations to realistic programming languages with rich binding forms is deemed infeasible. This is a pity, because we lose the practical benefits of mechanizing real programming languages.

We present a new solution to generically handle the boilerplate involved in mechanizations that scales to rich binding forms and advanced rules of scoping. We define a new specification language for abstract syntax with binding and implement a code generator that produces Coq code for the representation of the abstract syntax, syntactic operations and proofs of their properties.

We illustrate how our approach removes the burden of variable binding boilerplate in the mechanization of realistic programming languages on a list of example specifications and a solution of the PoplMark challenge based on the generated code.

BibTeX

@unpublished{infragen,
  author = "Keuchel, Steven and Weirich, Stephanie and 
            Schrijvers, Tom",
  title =  "{InfraGen: Binder Boilerplate at Scale}",
  year =   "2014",
  note =   "Unpublished Draft",
  url =    "https://skeuchel.me/publication/2014-draft-infragen-binder-boilerplate-at-scale"
}