Higher-order representations of objects such as programs, specifications and proofs are important to many metaprogramming and symbolic computation tasks. Systems that support such representations often depend on the implementation of an intensional view of the terms of suitable typed lambda calculi. Refined lambda calculus notations have been proposed that can be used in realizing such implementations. There are, however, choices in the actual deployment of such notations whose practical consequences are not well understood. Towards addressing this lacuna, the impact of three specific ideas is examined:the de Bruijn representation of bound variables, the explicit encoding of substitutions in terms and the annotation of terms to indicate their independence on external abstractions. Qualitative assessments are complemented by experiments over actual computations. The empirical study is based on λProlog programs executed using suitable variants of a low level, abstract machine based implementation of this language.
|Original language||English (US)|
|Title of host publication||Rewriting Techniques and Applications - 13th International Conference, RTA 2002, Proceedings|
|Number of pages||15|
|ISBN (Print)||3540439161, 9783540439165|
|State||Published - 2002|
|Event||13th International Conference on Rewriting Techniques and Applications, RTA 2002 - Copenhagen, Denmark|
Duration: Jul 22 2002 → Jul 24 2002
|Name||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|Other||13th International Conference on Rewriting Techniques and Applications, RTA 2002|
|Period||7/22/02 → 7/24/02|
Bibliographical notePublisher Copyright:
© Springer-Verlag Berlin Heidelberg 2002.