From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id JAA18720 for caml-red; Fri, 6 Oct 2000 09:36:27 +0200 (MET DST) Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id BAA19227 for ; Fri, 6 Oct 2000 01:29:42 +0200 (MET DST) Received: from fledge.watson.org (fledge.watson.org [204.156.12.50]) by nez-perce.inria.fr (8.10.0/8.10.0) with ESMTP id e95NTfP10582 for ; Fri, 6 Oct 2000 01:29:41 +0200 (MET DST) Received: from localhost (patrick@localhost) by fledge.watson.org (8.9.3/8.9.3) with SMTP id TAA51235; Thu, 5 Oct 2000 19:29:30 -0400 (EDT) (envelope-from patrick@watson.org) Date: Thu, 5 Oct 2000 19:29:30 -0400 (EDT) From: Patrick M Doane To: David McClain cc: caml-list@inria.fr Subject: Re: de Bruijn indices Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: weis@pauillac.inria.fr > 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