Normalization by Evaluation
Andreas Abel
Institut für Informatik
Ludwig-Maximilians-Universität München
Monday, 6 April 2009, 14:00 (note the unusual weekday)
Cybernetica Bldg (Akadeemia tee 21), room B101
Slides from the talk [pdf]
Abstract: Normalization by evaluation is a technique to compute the full beta-normal form of lambda-terms. In the first step, terms are interpreted in some value domain, which corresponds to computing a semantic weak head normal form. In the second step, values are reified, i.e., converted back to terms which are actually normal forms. During reification, evaluation under binders takes place.
In this talk, I will first give a tutorial on normalization by evaluation for the simply-typed lambda-calculus. I review interpretation of lambda-terms into an applicative structure and then define a simple type-directed reification which returns eta-long beta-normal forms. I sketch the proof of soundness and completeness which involves constructions of Kripke logical relations. The proof is generic enough to account for related results, like weak beta-(eta-)normalization.
In the last part of my talk, I outline how to extend normalization by evaluation to System F, the polymorphic lambda-calculus, using Girard's idea.
Tarmo Uustalu
Last update 6.4.2009