# COQ files for TYPES 2006 article

The following files are the Coq development for the results reported
in the article *Combining de Bruijn Indices and Higher-Order
Abstract Syntax in Coq* by Venanzio Capretta and Amy P. Felty, to
appear in the Proceedings of TYPES 2006.
De Bruijn syntax is needed for the Lambda Calculus and Quantified
Propositional Logic. You need first to compile *deBruijn.v*
with the command:

**coqc deBruijn.v**

to be able to run *Lambda.v* and *QPL.v*.