http://www.mathnet.ru/conf664
1. λ-термы. Бестиповое λ-исчисление. α-конверсия и β-редукция.
2. Граф редукций λ-терма. Свойство Чёрча–Россера. Нормальные формы. Единственность нормальной формы. Примеры λ-термов, не имеющих нормальной формы.
3. Теорема о неподвижной точки для бестипового Лямбда-исчисления. Равномерная теорема о неподвижной точке (комбинатор неподвижной точки).
4. Кодирование натуральных чисел и представимость вычислимых функций в бестиповом Лямбда-исчислении. Неразрешимость проблемы нормализуемости.
5. Типовое λ-исчисление (варианты с жесткой типизацией и с мягкой типизацией в стиле Карри и Чёрча). Слабая нормализуемость.
6. Теорема о сильной нормализуемости для типового λ-исчисления.
7. η-редукция. Теоретико-множественная интерпретация типового λ-исчисления с правилом η-редукции; теорема о полноте.
8. Введение в теорию категорий. Декартово замкнутые категории. Интерпретация типового λ-исчисления без правила η-редукции на декартово замкнутых категориях; теорема о полноте.
9. Интуиционистская логика высказываний. Неформальная семантика Брауэра–Гейтинга–Колмогорова (BHK). Семантика Крипке, теорема о полноте. Теорема Гливенко.
Ф.Н. Пахомов
10. Система естественного вывода для импликативного фрагмента интуиционистской логики высказываний. Соответствие Карри–Говарда (формулы как типы, термы как доказательства).
Д.С. Шамканов
11. Гильбертовское исчисление для интуиционистской логики высказываний и комбинаторная логика. Перевод из типового λ-исчисления в комбинаторную логику.
12. Генценовское (секвенциальное) исчисление для интуиционистской логики высказываний. Теорема об устранении сечения.
Интуиционистская логика первого порядка. Система естественного вывода и генценовское (секвенциальное) исчисление.