Adam Chlipala

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2007-147

December 11, 2007

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-147.pdf

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 <i>proof by reflection</i>, requires users to trust none of its associated code to be able to trust in the validity of theorems derived with it.

---

BibTeX citation:

@techreport{Chlipala:EECS-2007-147,
    Author= {Chlipala, Adam},
    Title= {Generic Programming and Proving for Programming Language Metatheory},
    Year= {2007},
    Month= {Dec},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-147.html},
    Number= {UCB/EECS-2007-147},
    Abstract= {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 <i>proof by reflection</i>, requires users to trust none of its associated code to be able to trust in the validity of theorems derived with it.},
}

EndNote citation:

%0 Report
%A Chlipala, Adam 
%T Generic Programming and Proving for Programming Language Metatheory
%I EECS Department, University of California, Berkeley
%D 2007
%8 December 11
%@ UCB/EECS-2007-147
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-147.html
%F Chlipala:EECS-2007-147