Personal tools
You are here: Home Events Abstract Archives 1999 Purely Syntactic Normalization by Evaluation

Purely Syntactic Normalization by Evaluation

René Vestergaard Department of Computing and Electrical Engineering Heriot-Watt University 4pm Tuesday 16 March 1999 Room 2511, JCMB, King's Buildings

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.

Document Actions