Proof Pearl: de Bruijn Terms Really Do Work

    Michael Norrish, NICTA   Rene Vestergaard, JAIST


Placing our result in a web of related mechanised results, we
give a direct proof that the de Bruijn lambda-calculus (a` la
Huet, Nipkow and Shankar) is isomorphic to an alpha-quotiented
lambda-calculus. In order to establish the link, 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 alpha-quotiented and
the proper de Bruijn formalisms draws on techniques from the
theory of nominal sets.