Name
Abstract | ||
|---|---|---|
We give an introduction to normalization by evaluation and type-directed partial evaluation. We first present normalization by evaluation for a combinatory version of G枚del System T. Then we show normalization by evaluation for typed lambda calculus with 脽 and 驴 conversion. Finally, we introduce the notion of binding time, and explain the method of type-directed partial evaluation for a small PCF-style functional programming language. We give algorithms for both call-byname and call-by-value versions of this language. |
Year | DOI | Venue |
|---|---|---|
2000 | 10.1007/3-540-45699-6_4 | APPSEM |
Keywords | Field | DocType |
lambda calculus,present normalization,del system t.,combinatory version,call-by-value version,small pcf-style functional programming,type-directed partial evaluation,partial evaluation,binding time,programming language,typed lambda calculus | Lambda calculus,Normalization (statistics),Functional programming,Gödel,Typed lambda calculus,Computer science,Partial evaluation,Type theory,Semantics,Calculus | Conference |
Volume | ISSN | ISBN |
2395 | 0302-9743 | 3-540-44044-5 |
Citations | PageRank | References |
19 | 0.99 | 29 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Peter Dybjer | 1 | 540 | 76.99 |
| Andrzej Filinski | 2 | 334 | 24.65 |