Проблемы разрешимости: проверка типа, синтез типа и населенность типа. Лемма об образовании редексов. Меры типа и терма. Слабая нормализация для $ \lambda_{\rightarrow} $. Сильная нормализация. Интерпретации $ {\rightarrow} $-типов. Расширение системы константами. $ \delta $-редукция.