Normalization by Evaluation

 

Title: Normalization by Evaluation
Authors: 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.
BibTeX:
@article{NormByEval-AFP,
  author  = {Klaus Aehlig and Tobias Nipkow},
  title   = {Normalization by Evaluation},
  journal = {Archive of Formal Proofs},
  month   = feb,
  year    = 2008,
  note    = {\url{http://isa-afp.org/entries/NormByEval.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License