Normalization by Evaluation

Klaus Aehlig 🌐 and Tobias Nipkow 🌐

February 18, 2008

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Related publications

  • AEHLIG, K., HAFTMANN, F., & NIPKOW, T. (2012). A compiled implementation of normalisation by evaluation. Journal of Functional Programming, 22(1), 9–30.
  • author's copy

Session NormByEval