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.