Normalization by Evaluation

Klaus Aehlig 🌐 and Tobias Nipkow 🌐

February 18, 2008

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: