Term rewriting for normalization by evaluation

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.

Authors

• Ulrich Berger
• Matthias Eberl
• Helmut Schwichtenberg

Keywords

No keywords are indexed for this paper.