Система $ \lambda_{\rightarrow} $. Предтермы. Отношение типизации. Контексты. Правила типизации по Карри и по Чёрчу. Деревья вывода типов. Система минимальной пропозициональной логики. Соответствие Карри-Говарда.