"Normalization by Evaluation" (nbe) is an approach to normalization in, as a rule, a certain version of lambda calculus, based on the evaluation in the metalanguage. Namely, a composition of a functional, inversing the evaluator, with that evaluator is an effective procedure for the normalization in the calculus in question. We consider the definition of nbe for basic typed calculi, its extension for the untyped case, and discuss the areas of its application.

Supplementary materials:

1. U. Berger, H. Schwichtenberg. An inverse to the evaluation functional for typed λ-calculus.

2. T. Altenkirch and T. Uustalu. Normalization by evaluation for λ→2.

3. U. Berger, M. Eberl, H. Schwichtenberg. Term rewriting for normalization by evaluation.

Presenter: Daniil Berezun

Date: February 12, 2018

Time: 17:15

Venue: room 3248, Faculty of Mathematics and Mechanics, Saint Petersburg State University, Stary Peterhof, Universitetski pr., 28