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

Proof outline Proof document

Browse theories

Download this entry

Older releases: Isabelle 2011: afp-NormByEval-2011-02-11.tar.gz Isabelle 2009-2: afp-NormByEval-2010-07-01.tar.gz Isabelle 2009-1: afp-NormByEval-2009-12-12.tar.gz Isabelle 2009: afp-NormByEval-2009-04-29.tar.gz Isabelle 2008: afp-NormByEval-2008-06-10.tar.gz Isabelle 2007: afp-NormByEval-2008-02-22.tar.gz Isabelle 2007: afp-NormByEval-2008-02-18.tar.gz