|
ИСТИНА |
Войти в систему Регистрация |
ИСТИНА ИНХС РАН |
||
Вычислительная теория доказательств и лямбда-исчислениеучебный курс
- Авторы: Беклемишев Лев Дмитриевич, Кузнецов Степан Львович
- Год создания: 2019
- Организация: Математический институт имени В. А. Стеклова РАН
- Описание: Бета-редукции. Свойство Чёрча‒Россера. Стратегии редукций. Слабая и сильная нормализуемость для типизованного лямбда-исчисления. Теорема о неподвижной точке для бестипового лямбда-исчисления. Кодирование рекурсивных функций. Алгоритм выведения типов для простого типового лямбда-исчисления. Эта-редукция. Теоретико-множественная интерпретация лямбдаисчисления, теорема о полноте. Интуиционистская логика высказываний. Семантика Крипке, теорема о полноте. Соответствие Карри‒Говарда. Исчисление гильбертовского типа и комбинаторная логика. Интерпретация типизованного лямбда-исчисления на декартово замкнутых категориях. Семантики Скотта и Ершова для бестипового лямбда-исчисления. ================================================== Сайт курса: http://www.mathnet.ru/conf1615
- Добавил в систему: Кузнецов Степан Львович