> Could you provide a reference to de Bruijin indexing? I recall reading
> about it some time ago, and after having searched my books here, I
> cannot find any references to it. So I probably saw it in a paper some
> time ago... Anyway, I would be interested since I have an interpreter
> name-lookup problem heretoo.

You should take a look at Frank Pfenning's course notes for his class on
Computation and Deduction. The chapter on compilation covers the use of de
Bruijn indices as well some interesting judgements abouts the compilation
process. This chapter is located at:

  http://www.cs.cmu.edu/~fp/courses/comp-ded/notes/chap6.pdf

The rest of the course notes are excellent for those interested in
formally representing theorems about programming languages in a logical
framework. 

Patrick Doane