# Normalization by Evaluation

 Title: Normalization by Evaluation Authors: Klaus Aehlig and Tobias Nipkow Submission date: 2008-02-18 Abstract: This article formalizes normalization by evaluation as implemented in Isabelle. Lambda calculus plus term rewriting is compiled into a functional program with pattern matching. It is proved that the result of a successful evaluation is a) correct, i.e. equivalent to the input, and b) in normal form. BibTeX: @article{NormByEval-AFP, author = {Klaus Aehlig and Tobias Nipkow}, title = {Normalization by Evaluation}, journal = {Archive of Formal Proofs}, month = feb, year = 2008, note = {\url{https://isa-afp.org/entries/NormByEval.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.