Леммы о контекстах. Типизируемость подтермов, нетипизируемые предтермы. Лемма подстановки. Теорема о редукции субъекта. Незамкнутость относительно экспансии. Уникальность типов для типизации по Чёрчу. Связь между системами Карри и Черча. Главный (наиболее общий) тип для $ \lambda_{\rightarrow} $ в стиле Карри. Свойства подстановки. Унификация. Алгоритм Хиндли-Милнера.