Abstract

We will give a strikingly simple presentation of Berger's and Schwichtenberg's Normalization by Evaluation technique. The correctness proof is carried out on a naïve, two-level lambda-calculus. The calculus is defined such that one level straightforwardly can be collapsed to a term model in a way that allows us to regain the slogan: "Normalization by Evaluation". No prior knowledge, except for familarity with the lambda-calculus, will be assumed.