С.Л. Кузнецов. Спецкурс «Лямбда-исчисление, или вычислительная теория доказательств»

Лекции и семинары Научно-образовательного центра Математического института им. В.А. Стеклова Российской академии наук.
С.Л. Кузнецов. Спецкурс «Лямбда-исчисление, или вычислительная теория доказательств».
Москва, МИАН, весна 2015 г.
Все лекции спецкурса: http://www.mathnet.ru/conf664.

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