RUS  ENG ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ЛИЧНЫЙ КАБИНЕТ


Спецкурс С. Л. Кузнецова «Лямбда-исчисление, или вычислительная теория доказательств», 2015
18 февраля–13 мая 2015 г., МИАН, ауд. 313 (ул. Губкина, 8), г. Москва

  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$-исчисления в языкознании: категориальные грамматики, семантика Монтегю.


Программа семинара

RSS: Ближайшие семинары

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

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


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

13 мая 2015 г.
1. Лямбда-исчисление, или вычислительная теория доказательств. Лекция 12
С. Л. Кузнецов
13 мая 2015 г. 18:00, г. Москва, МИАН, ауд. 313 (ул. Губкина, 8)
С. Л. Кузнецов
  

29 апреля 2015 г.
2. Лямбда-исчисление, или вычислительная теория доказательств. Лекция 11
С. Л. Кузнецов
29 апреля 2015 г. 18:05, г. Москва, МИАН, ауд.515 (ул.Губкина, 8)
С. Л. Кузнецов
  

22 апреля 2015 г.
3. Лямбда-исчисление, или вычислительная теория доказательств. Лекция 10
Д. С. Шамканов
22 апреля 2015 г. 18:00, г. Москва, МИАН, ауд. 313 (ул. Губкина, 8)
Д. С. Шамканов
  

15 апреля 2015 г.
4. Лямбда-исчисление, или вычислительная теория доказательств. Лекция 9
Ф. Н. Пахомов
15 апреля 2015 г. 18:00, г. Москва, МИАН, ауд. 313 (ул. Губкина, 8)
Ф. Н. Пахомов
  

8 апреля 2015 г.
5. Лямбда-исчисление, или вычислительная теория доказательств. Лекция 8
С. Л. Кузнецов
8 апреля 2015 г. 18:00, г. Москва, МИАН, ауд. 313 (ул. Губкина, 8)
С. Л. Кузнецов
  

1 апреля 2015 г.
6. Лямбда-исчисление, или вычислительная теория доказательств. Лекция 7
С. Л. Кузнецов
1 апреля 2015 г. 18:00, г. Москва, МИАН, ауд. 313 (ул. Губкина, 8)
С. Л. Кузнецов
  

25 марта 2015 г.
7. Лямбда-исчисление, или вычислительная теория доказательств. Лекция 6
С. Л. Кузнецов
25 марта 2015 г. 18:00, г. Москва, МИАН, ауд. 313 (ул. Губкина, 8)
С. Л. Кузнецов
  

18 марта 2015 г.
8. Лямбда-исчисление, или вычислительная теория доказательств. Лекция 5
С. Л. Кузнецов
18 марта 2015 г. 18:00, г. Москва, МИАН, ауд. 313 (ул. Губкина, 8)
С. Л. Кузнецов
  

11 марта 2015 г.
9. Лямбда-исчисление, или вычислительная теория доказательств. Лекция 4
С. Л. Кузнецов
11 марта 2015 г. 18:00, г. Москва, МИАН, ауд. 313 (ул. Губкина, 8)
С. Л. Кузнецов
  

4 марта 2015 г.
10. Лямбда-исчисление, или вычислительная теория доказательств. Лекция 3
С. Л. Кузнецов
4 марта 2015 г. 18:00, г. Москва, МИАН, ауд. 313 (ул. Губкина, 8)
С. Л. Кузнецов
  

25 февраля 2015 г.
11. Лямбда-исчисление, или вычислительная теория доказательств. Лекция 2
С. Л. Кузнецов
25 февраля 2015 г. 18:00, г. Москва, МИАН, ауд. 313 (ул. Губкина, 8)
С. Л. Кузнецов
  

18 февраля 2015 г.
12. Лямбда-исчисление, или вычислительная теория доказательств. Лекция 1
С. Л. Кузнецов
18 февраля 2015 г. 18:00, г. Москва, МИАН, ауд. 313 (ул. Губкина, 8)
С. Л. Кузнецов
  
 
Обратная связь:
 Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2017