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.
- AEHLIG, K., HAFTMANN, F., & NIPKOW, T. (2012). A compiled implementation of normalisation by evaluation. Journal of Functional Programming, 22(1), 9–30. https://doi.org/10.1017/s0956796812000019
- author's copy