A Head-to-Head Comparison of de Bruijn Indices and Names

Often debates about pros and cons of various techniques for formalising lambda-calculi rely on subjective arguments, such as de Bruijn indices are hard to read for humans or nominal approaches come close to the style of reasoning employed in informal proofs. In this paper we will compare four formalisations based on de Bruijn indices and on names from the nominal logic work, thus providing some hard facts about the pros and cons of these two formalisation techniques. We conclude that the relative merits of the different approaches, as usual, depend on what task one has at hand and which goals one pursues with a formalisation. Key words: Proof assistants, lambda-calculi, de Bruijn indices, nominal logic work, Isabelle/HOL.

• Type: Journal
• Year: 2007
• Where: ENTCS
• Authors: Stefan Berghofer, Christian Urban
• Keywords: Bruijn Indices, ENTCS 2007, Nominal Approaches, Nominal Logic Work