Proof Pearl: De Bruijn Terms Really Do Work

Placing our result in a web of related mechanised results, we give a direct proof that the de Bruijn λ-calculus (`a la Huet, Nipkow and Shankar) is isomorphic to an α-quotiented λ-calculus. In order to establink, we introduce an “index-carrying” abstraction mechanism over de Bruijn terms, and consider it alongside a simplified substitution mechanism. Relating the new notions to those of the α-quotiented and the proper de Bruijn formalisms draws on techniques from the theory of nominal sets.

• Type: Conference
• Year: 2007
• Where: TPHOL
• Authors: Michael Norrish, René Vestergaard
• Keywords: A La Huet, Artificial Intelligence, Bruijn λ-calculus, Simplified Substitution Mechanism, TPHOL 2007