Normalization by Evaluation

Klaus Aehlig 🌐 and Tobias Nipkow 🌐

February 18, 2008

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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

Topics

Related publications

  • AEHLIG, K., HAFTMANN, F., & NIPKOW, T. (2012). A compiled implementation of normalisation by evaluation. Journal of Functional Programming, 22(1), 9–30. https://doi.org/10.1017/s0956796812000019
  • author's copy

Session NormByEval

Cite

× 
@article{NormByEval-AFP,
  author  = {Klaus Aehlig and Tobias Nipkow},
  title   = {Normalization by Evaluation},
  journal = {Archive of Formal Proofs},
  month   = {February},
  year    = {2008},
  note    = {\url{https://isa-afp.org/entries/NormByEval.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: