A Head-to-Head Comparison of de Bruijn Indices and Names |
| |
Authors: | Stefan Berghofer Christian Urban |
| |
Affiliation: | aInstitut für Informatik, Technische Universität München, Boltzmannstraße 3, 85748 Garching, Germany |
| |
Abstract: | 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. |
| |
Keywords: | Proof assistants lambda-calculi de Bruijn indices nominal logic work Isabelle/HOL |
本文献已被 ScienceDirect 等数据库收录! |
|