@article{Berger200319,
    Abstract = {We extend normalization by evaluation (first presented in [5]) from the pure typed {$\lambda$}-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.},
    Author = {Berger, Ulrich and Eberl, Matthias and Schwichtenberg, Helmut},
    File = {1-s2.0-S0890540103000142-main (0) - a - a - g.pdf},
    ISSN = {0890-5401},
    Journal = {Information and Computation},
    Keywords = {normalization by evaluation and readme},
    Note = {International Workshop on Implicit Computational Complexity (ICC'99)},
    Number = {1},
    Pages = {19 - 42},
    Title = {Term rewriting for normalization by evaluation},
    URL = {http://www.sciencedirect.com/science/article/pii/S0890540103000142},
    Volume = {183},
    Year = {2003},
    bdsk-url-1 = {http://www.sciencedirect.com/science/article/pii/S0890540103000142},
    bdsk-url-2 = {https://doi.org/10.1016/S0890-5401(03)00014-2},
    date-added = {2017-05-01 20:00:31 +0000},
    date-modified = {2017-05-01 20:00:53 +0000},
    doi = {10.1016/S0890-5401(03)00014-2}
}

@article{Berger200319, Abstract = {We extend normalization by evaluation (first presented in [5]) from the pure typed {$\lambda$}-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.}, Author = {Berger, Ulrich and Eberl, Matthias and Schwichtenberg, Helmut}, File = {1-s2.0-S0890540103000142-main (0) - a - a - g.pdf}, ISSN = {0890-5401}, Journal = {Information and Computation}, Keywords = {normalization by evaluation and readme}, Note = {International Workshop on Implicit Computational Complexity (ICC'99)}, Number = {1}, Pages = {19 - 42}, Title = {Term rewriting for normalization by evaluation}, URL = {http://www.sciencedirect.com/science/article/pii/S0890540103000142}, Volume = {183}, Year = {2003}, bdsk-url-1 = {http://www.sciencedirect.com/science/article/pii/S0890540103000142}, bdsk-url-2 = {https://doi.org/10.1016/S0890-5401(03)00014-2}, date-added = {2017-05-01 20:00:31 +0000}, date-modified = {2017-05-01 20:00:53 +0000}, doi = {10.1016/S0890-5401(03)00014-2} }