JetBrains Research — наука, меняющая мир

Семинар по нормализации путем вычислений

"Normalization by Evaluation" (nbe) представляет собой подход к нормализации термов, как правило того или иного лямбда-исчисления, основанный на механизме вычисления в мета-языке. А именно, композиция функционала, обращающего вычислитель, с самим вычислителем представляет собой эффективный алгоритм нормализации рассматриваемого исчисления. Мы рассмотрим как определяется nbe для базовых типизированных вычислений, как он распространяется на нетипизированное лямбда-исчисление, а также обсудим области его применения.

Материалы к докладу:

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.

Докладчик: Даниил Березун

12.02.2018, 17:15.

Место: ауд. 3248, мат-мех. факультет СПбГУ, Старый Петергоф, Университетский пр-т, д. 28