Tradeoffs in the intensional representation of lambda terms

Chuck Liang, Gopalan Nadathur

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Scopus citations


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 languageEnglish (US)
Title of host publicationRewriting Techniques and Applications - 13th International Conference, RTA 2002, Proceedings
EditorsSophie Tison
PublisherSpringer Verlag
Number of pages15
ISBN (Print)3540439161, 9783540439165
StatePublished - 2002
Event13th International Conference on Rewriting Techniques and Applications, RTA 2002 - Copenhagen, Denmark
Duration: Jul 22 2002Jul 24 2002

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other13th International Conference on Rewriting Techniques and Applications, RTA 2002

Bibliographical note

Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2002.


Dive into the research topics of 'Tradeoffs in the intensional representation of lambda terms'. Together they form a unique fingerprint.

Cite this