Copenhagen Programming Language Seminar

Normalization by evaluation for System F

Andreas Abel
Ludwig-Maximilians-Universität München

Friday 30 January 2009, 10:30-11:30
The IT University, Rued Langgaards Vej 7, DK-2300 Room 3A.14


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.

Scientific host:Carsten Schürmann Administrative host: Annette Enggaard. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU, KVL and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org