zbMATH — the first resource for mathematics

Term rewriting for normalization by evaluation. (English) Zbl 1054.68078
Summary: We extend normalization by evaluation from the pure typed \(\lambda\)-calculus to general higher type term rewriting systems and prove its correctness with respect to 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.

68Q42 Grammars and rewriting systems
68N18 Functional programming and lambda calculus
Full Text: DOI
[1] Altenkirch, T.; Hofmann, M.; Streicher, T., Categorical reconstruction of a reduction free normalization proof, (), 182-199
[2] Benl, H.; Berger, U.; Schwichtenberg, H.; Seisenberger, M.; Zuber, W., Proof theory at work: program development in the minlog system, (), 41-71 · Zbl 1015.68177
[3] U. Berger, Continuous functionals of dependent and transfinite types, Habilitationsschrift, Mathematisches Institut der Universität München, 1997 · Zbl 0946.03068
[4] Berger, U.; Eberl, M.; Schwichtenberg, H., Normalization by evaluation, (), 117-137
[5] Berger, U.; Schwichtenberg, H., An inverse of the evaluation functional for typed λ-calculus, (), 203-211
[6] Coquand, T.; Dybjer, P., Intuitionistic model constructions and normalization proofs, Math. struct. comput. sci., 7, 73-94, (1997) · Zbl 0883.03009
[7] Crole, R.L., Categories for types, (1993), Cambridge University Press Cambridge · Zbl 0837.68077
[8] Danvy, O., Pragmatics of type-directed partial evaluation, (), 73-94
[9] de Bruijn, N.G., Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem, Indagationes math., 34, 381-392, (1972) · Zbl 0253.68007
[10] Filinski, A., A semantic account of type-directed partial evaluation, (), 378-395 · Zbl 0953.68034
[11] Lambek, I.; Scott, P., Introduction to higher order categorical logic, Cambridge studies in advanced mathematics, vol. 7, (1986), Cambridge University Press Cambridge, UK · Zbl 0596.03002
[12] McCarthy, J., Recursive functions of symbolic expressions and their computation by machine, Commun. assoc. comput. Mach., 3, 4, 184-195, (1960) · Zbl 0101.10413
[13] Plotkin, G.D., LCF considered as a programming language, Theoret. comput. sci., 5, 223-255, (1977) · Zbl 0369.68006
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.