Name
Abstract | ||
|---|---|---|
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. |
Year | Venue | Keywords |
|---|---|---|
2002 | RTA | lambda terms,de bruijn representation,lambda calculus,suitable variant,actual deployment,intensional representation,refined lambda calculus notation,abstract machine,empirical study,bound variable,higher-order representation,actual computation,symbolic computation,higher order |
Field | DocType | Volume |
Metaprogramming,Lambda calculus,Programming language,Functional programming,Computer science,Algorithm,Symbolic computation,Theoretical computer science,Mathematical proof,Prolog,Logic programming,Abstract machine | Conference | 2378 |
ISSN | ISBN | Citations |
0302-9743 | 3-540-43916-1 | 7 |
PageRank | References | Authors |
0.58 | 13 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Chuck Liang | 1 | 145 | 8.70 |
| Gopalan Nadathur | 2 | 1047 | 117.85 |