Normalization by Evaluation (Q7361317)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry NormByEval
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Normalization by Evaluation |
AFP entry NormByEval |
Statements
18 February 2008
0 references
Klaus Aehlig
0 references
Tobias Nipkow
0 references
Normalization by Evaluation (English)
0 references
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.
0 references
