Normalization by Evaluation

Klaus Aehlig and Tobias Nipkow

18 February 2008

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.
BSD License

Topics

Theories