The terms `normalization by evaluation', `normalization by intuitionistic model construction', `reduction-free normalization', and `type-directed partial evaluation' all designate a very concise and elegant specification of normalization in the lambda-calculus where normalization steps are carried out in the meta-language. The idea originates in the area of logic and proof theory, and recently, it has surfaced in the area of programming languages. The goal of this workshop is to bring together all people who have discovered and/or worked with normalization by evaluation.
Organizers: Olivier Danvy and Peter Dybjer.