The concept of normalization by evaluation (NBE) has seen significant interest in the last few years. In this talk, I will present the basic idea of reduction-free normalization of lambda-terms, and sketch how it can be reduced to standard evaluation using NBE. I will also outline how NBE can be used to achieve a form of cogen-based partial evaluation in higher-order functional languages with general recursion and interpreted constants.

This talk is intended to serve as an overview and tutorial, rather than to present the latest technical results. Basic familiarly with the simply-typed lambda calculus and its semantics, and/or general partial-evaluation concepts will be helpful, but not essential.