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

@inproceedings{citeulike:1303365, 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.}, author = {Berghofer, Stefan and Urban, Christian}, booktitle = {International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice}, citeulike-article-id = {1303365}, citeulike-linkout-0 = {http://www.easychair.org/FLoC-06/LFMTP-preproceedings.pdf}, keywords = {metaprogramming}, posted-at = {2007-05-17 17:58:49}, priority = {2}, title = {A Head-to-Head Comparison of de Bruijn Indices and Names}, url = {http://www.easychair.org/FLoC-06/LFMTP-preproceedings.pdf}, year = {2006} }

TY - CONF ID - citeulike:1303365 L3 - citeulike-article-id:1303365 N2 - 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. TI - A Head-to-Head Comparison of de Bruijn Indices and Names T2 - International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice KW - metaprogramming AU - Berghofer, Stefan AU - Urban, Christian PY - 2006/// UR - http://www.easychair.org/FLoC-06/LFMTP-preproceedings.pdf ER -