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


Вычислительная теория доказательств и лямбда-исчисление
МИАН, комн. 530 (ул. Губкина, 8), г. Москва

Курс планируется как годовой. В первой части (осенний семестр) планируется изложить основы лямбда-исчисления и его связь с системой естественного вывода для интуиционистской логики (соответствие Карри‒Говарда).
Примерный список тем первого семестра:

  1. Бета-редукции. Свойство Чёрча‒Россера. Стратегии редукций. Слабая и сильная нормализуемость для типизованного лямбда-исчисления.
  2. Теорема о неподвижной точке для бестипового лямбда-исчисления. Кодирование рекурсивных функций.
  3. Алгоритм выведения типов для простого типового лямбда-исчисления.
  4. Эта-редукция. Теоретико-множественная интерпретация лямбдаисчисления, теорема о полноте.
  5. Интуиционистская логика высказываний. Семантика Крипке, теорема о полноте. Соответствие Карри‒Говарда.
  6. Исчисление гильбертовского типа и комбинаторная логика.
  7. Интерпретация типизованного лямбда-исчисления на декартово замкнутых категориях.
  8. Семантики Скотта и Ершова для бестипового лямбда-исчисления.


Программа

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

Руководители семинара
Беклемишев Лев Дмитриевич
Кузнецов Степан Львович

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

 
Обратная связь:
 Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2019