Name
Abstract | ||
|---|---|---|
Closed reductions in the λ-calculus is a strategy for a calculus of explicit substitutions which overcomes many of the usual syntactical problems of substitution. This is achieved by only moving closed substitutions through certain constructs, which gives a weak form of reduction, but is rich enough to capture the usual strategies in the λ-calculus (call-by-value, call-by-need, etc.) and is adequate for the evaluation of programs. An interesting point is that the calculus permits substitutions to move through abstractions, and reductions are allowed under abstractions, if certain conditions hold. The calculus naturally provides an efficient notion of reduction (with a high degree of sharing), which can easily be implemented. |
Year | Venue | Keywords |
|---|---|---|
1999 | CSL | high degree,closed reductions,certain construct,calculus permits substitution,closed substitution,closed reduction,usual strategy,certain condition,usual syntactical problem,explicit substitution,efficient notion,lambda calculus |
Field | DocType | ISBN |
Discrete mathematics,Combinatorics,Lambda calculus,Abstraction,Computer science | Conference | 3-540-66536-6 |
Citations | PageRank | References |
11 | 0.76 | 8 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Maribel Fernández | 1 | 315 | 23.44 |
| Ian Mackie | 2 | 88 | 9.58 |