We present a system for both the generic programming of operations that work over classes of tree-structured data types and the automatic generation of formal type-theoretical proofs about such operations. The system is implemented in the Coq proof assistant, using dependent types to validate code and proof generation statically, quantified over all possible input data types. We focus on generic programming of variable-manipulating operations, such as substitution and free variable set calculation, over abstract syntax tree types implemented as GADTs that combine syntax and typing rules. By accompanying these operations with generic lemmas about their interactions, we significantly ease the burden of formalizing programming language metatheory. Our implementation strategy, based on proof by reflection, requires users to trust none of its associated code to be able to trust in the validity of theorems derived with it.
Slides are available from a talk I gave at WMM'07, in OpenOffice and PDF formats.