Лаборатория языковых инструментов

Линейная заголовочная редукция (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.

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