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.
  author  = {Klaus Aehlig and Tobias Nipkow},
  title   = {Normalization by Evaluation},
  journal = {Archive of Formal Proofs},
  month   = feb,
  year    = 2008,
  note    = {\url{},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.