Исследовательская группа
Лаборатория языковых инструментов
Линейная заголовочная редукция
28 марта
Линейная заголовочная редукция (head linear reduction) представляет собой один из подходов к нормализации лямбда-выражений, реализация которого не нужнается в таких традиционных техниках, как \beta-редукции в классическом понимании последних, замыканиях и окружениях. В докладе будет рассмотрен алгоритм нормализации для STLC, основанный на head linear reduction, а также представлено его обобщение для нетипизированного лямбда-исчисления.
Материалы к докладу:
1. Vincent Danos, Laurent Regnier. Head Linear Reduction, 2004.
2. C.-H. Luke Ong. Normalisation by traversals. CoRR, abs/1511.02629, 2015.
Докладчик: Даниил Березун.