Name
Abstract | ||
|---|---|---|
We extend normalization by evaluation (first presented in [5]) from the pure typed λ-calculus to general higher type term rewriting systems and prove its correctness w.r.t. a domain-theoretic model. We distinguish between computational rules and proper rewrite rules. The former is a rather restricted class of rules, which, however, allows for a more efficient implementation. |
Year | DOI | Venue |
|---|---|---|
2003 | 10.1016/S0890-5401(03)00014-2 | Information and Computation/information and Control |
Keywords | Field | DocType |
general higher type term,correctness w,efficient implementation,computational rule,restricted class,domain-theoretic model | Lambda calculus,Normalization (statistics),Correctness,Slide rule,Rewriting,Confluence,Standardization,Mathematics,Calculus,Mathematical logic | Journal |
Volume | Issue | ISSN |
183 | 1 | Information and Computation |
Citations | PageRank | References |
14 | 0.95 | 8 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ulrich Berger | 1 | 151 | 19.55 |
| Matthias Eberl | 2 | 42 | 3.37 |
| Helmut Schwichtenberg | 3 | 373 | 44.83 |