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.
Title
Generic Programming and Proving for Programming Language Metatheory
Published
2007-12-11
Full Collection Name
Electrical Engineering & Computer Sciences Technical Reports
Other Identifiers
EECS-2007-147
Type
Text
Extent
15 p
Archive
The Engineering Library
Usage Statement
Researchers may make free and open use of the UC Berkeley Library’s digitized public domain materials. However, some materials in our online collections may be protected by U.S. copyright law (Title 17, U.S.C.). Use or reproduction of materials protected by copyright beyond that allowed by fair use (Title 17, U.S.C. § 107) requires permission from the copyright owners. The use or reproduction of some materials may also be restricted by terms of University of California gift or purchase agreements, privacy and publicity rights, or trademark law. Responsibility for determining rights status and permissibility of any use or reproduction rests exclusively with the researcher. To learn more or make inquiries, please see our permissions policies (https://www.lib.berkeley.edu/about/permissions-policies).
