## Normalization by Evaluation

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