Normalization by Evaluation

Title:	Normalization by Evaluation
Author:	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.
Status: [ok]	This is the development version of this entry generated for Isabelle-25-Dec-2009. The development version might change over time and is only permanently archived at Isabelle release points. It is provided as a preview of the next upcoming release. Please refer to release versions only in citations. If the status shows [FAIL], the links below will point to the last working version if any.

Older releases: