@inproceedings{capretta/felty:2006, author = {Venanzio Capretta and Amy Felty}, title = {Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq}, booktitle = {Proceedings of TYPES 2006}, editor = {Thorsten Altenkirch and Conor McBride}, series = {LNCS}, volume = {4502}, publisher = {Springer}, pages = {63--77}, year = 2007 }