1. $\lambda$-термы. Бест
   иповое $\lambda$-исчисление. $\alpha$-конверсия и $\beta$-редукция.
2. Граф редукций $\lambda$-терма. Свойство Чёрча–Россера. Нормальные формы. Единственность нормальной формы. Примеры $\lambda$-термов, не имеющих нормальной формы.
3. Теорема о неподвижной точки для бестипового $\lambda$-исчисления. Равномерная теорема о неподвижной точке (комбинатор неподвижной точки).
4. Кодирование натуральных чисел и представимость вычислимых функций в бестиповом $\lambda$-исчислении. Неразрешимость проблемы нормализуемости.
5. Т
   иповое $\lambda$-исчисление (варианты с жесткой типизацией и с мягкой типизацией в стиле Карри и Чёрча). Слабая нормализуемость.
6. Теорема о сильной нормализуемости для типового $\lambda$-исчисления.
7. $\eta$-редукция. Теоретико-множественная интерпретация типового $\lambda$-исчисления с правилом $\eta$-редукции; теорема о полноте.
8. Введение в теорию категорий. Декартово замкнутые категории. Интерпретация типового $\lambda$-исчисления без правила $\eta$-редукции на декартово замкнутых категориях; теорема о полноте.
9. Интуиционистская логика высказываний. Неформальная семантика Брауэра–Гейтинга–Колмогорова (BHK). Семантика Крипке, теорема о полноте. Теорема Гливенко.
10. Система естественного вывода для импликативного фрагмента интуиционистской логики высказываний. Соответствие Карри–Говарда (формулы как типы, термы как доказательства).
11. Гильбертовское исчисление для интуиционистской логики высказываний и комбин
    аторная логика. Перевод из типового $\lambda$-исчисления в комбинаторную логику.
12. Генценовское (секвенциальное) исчисление для интуиционистской логики высказываний. Теорема об устранении сечения.
13. Интуиционистская логика первого порядка. Система естественного вывода и генценовское (секвенциальное) исчисление.
14. Введение в теорию типов. Зависимое произведение типов и соответствие (по Карри–Говарду) с интуиционистским квантором всеобщности. Исчисление индуктивных конструкций (CIC); система Coq для формализации математических доказательств на ЭВМ.
15. Применение $\lambda$-исчисления в языкознании: категориальные грамматики, семантика Монтегю.

Программа

Руководитель
Кузнецов Степан Львович

Организации
Математический институт им. В.А. Стеклова Российской академии наук, г. Москва