Виталий Николаевич Брагилевский
Соответствие Карри–Ховарда:
от математической логики к программированию
В. Н. Брагилевский планирует провести 4 занятия.
Доступны 4 видеозаписи курса.
В программировании есть область, тесно связанная с математической логикой и другими разделами математики, — это верификация программного обеспечения, то есть проверка корректности программы относительно некоторой формальной спецификации. В наиболее жёстком режиме верификация превращается в доказательство теорем о правильности результатов работы программ. В этом курсе мы посмотрим на те математические основания, которые делают возможной именно такую верификацию.
Курс начнётся с элементарного введения в интуиционистскую логику и теорию доказательств, в рамках которого мы рассмотрим основные логические связки и правила вывода, а также построение с их помощью деревьев вывода, то есть собственно доказательств. После этого мы перейдём к изучению лямбда-исчисления как модели вычислений (эквивалентной, как известно, машине Тьюринга): мы определим множество лямбда-термов, обсудим понятия подстановки, альфа-эквивалентности и бета-редукции, после чего построим на этой базе простейший язык программирования.
Следующий шаг будет состоять в добавлении к лямбда-исчислению системы типов — так мы получим сначала простое типизированное лямбда-исчисление, а затем и некоторые наиболее важные его расширения. Лямбда-исчисление с типами оказывается удивительным образом связано с теорией доказательств: существует прямая связь между высказываниями и типами, а также между доказательствами и термами (программами) — мы увидим, что «доказывать теорему» означает в точности то же самое, что и «писать программу». Эту связь называют соответствием или изоморфизмом Карри–Ховарда, именно она делает возможными разработку и использование систем автоматического и интерактивного доказательства теорем. Наш курс завершится обзором и небольшой демонстрацией возможностей одной из таких систем, которая называется Coq: с её помощью мы формально докажем одну из математических теорем и построим доказуемо корректную реализацию одного из алгоритмов.
Этот курс не требует предварительных знаний вне стандартной школьной программы по математике и информатике, все используемые в нём понятия будут введены непосредственно по ходу. Курс будет сопровождаться упражнениями.
Материалы
Программа курсов и семинаров МЦНМО-НМУ в весеннем семестре 2024/2025 года
Расписание занятий в этом семестре
Курсы, читавшиеся в НМУ в разные годы (All Courses)
Если не указано иное, то начало занятий 7 февраля 2025.
Все обязательные курсы, почти все спецкурсы и некоторые доклады на спецсеминарах будут записываться на видео. Они будут доступны на общедоступном ресурсе.
К ВИДЕО-записям курсов этого семестра
Обязательные курсы
Первый курс
- Константин Валерьевич Логинов
- Алгебра-2
- читается по понедельникам с 17:30, очно+трансляция.
- Георгий Черных
- Топология-1
- читается по четвергам с 17:30, очно+трансляция.
- Олег Карлович Шейнман
- Математический анализ-2
- читается по пятницам с 17:30, очно+трансляция.
Второй курс
- Тарас Евгеньевич Панов
- Топология-3
- читается по понедельникам с 17:30 (семинары с 19:20), очно+трансляция
- Алексей Викторович Пенской
- Дифференциальная геометрия
- читается по средам с 17:30 (семинары с 19:20), очно+трансляция
- Алексей Игоревич Ильин
- Алгебра-4 (Группы и алгебры Ли)
- читается по четвергам с 17:30, очно+трансляция.
Список спецкурсов и спецсеминаров в весеннем семестре 2024/2025 года
- Михаил Юрьевич Розенблюм
- Алгебраическая теория чисел: введения. Продолжение годового спецкурса
- Денис Николаевич Терешкин
- Аддитивные и абелевы категории. Спецкурс рекомендован для 3-5 курсов.
- Константин Валерьевич Логинов
- Введение в ограниченность многообразий Фано. Спецкурс рекомендован для 3-5 курсов.
- Георгий Игоревич Шарыгин
- Циклические гомологии и их применения. Спецкурс рекомендован для 3-5 курсов.
- Андроник Арамович Арутюнов
- Грубая геометрия. Спецкурс в формате лекция + семинар, рекомендован для 3-5 курсов.
- Андрей Дмитриевич Рябичев
- Введение в поверхности бесконечного типа. Спецкурс рекомендован для 3-5 курсов.
- Георгий Борисович Шабат
- Тэта-функции и решетки. Часть 2. Спецкурс рекомендован для 3-5 курсов.
- Тарас Евгеньевич Панов
- Торическая топология, комбинаторика и теория гомотопий. Спецсеминар
- Георгий Игоревич Шарыгин и др.
- Деформационное квантование и квантовые группы. Спецсеминар
- А.М.Вербовецкий и И.С.Красильщик
- Когомологические аспекты геометрии дифференциальных уравнений,
руководители А.М.Вербовецкий и И.С.Красильщик - Николай Германович Мощевитин
- Диофантовы приближения. Спецсеминар рекомендован для 3-5 курсов
- Владимир Олегович Медведев
- Геометрия общей теории относительности. Спецкурс совместно с матфаком ВШЭ, рекомендован для 3-5 курсов.
- Алексей Викторович Пенской
- Риманова геометрия. Спецкурс совместно с матфаком ВШЭ, рекомендован для 3-5 курсов.
- Александр Борисович Калмынин
- Методы решета. Спецкурс рекомендован для 3-5 курсов.
- Алексей Викторович Пенской
- Спектральная геометрия. Спецсеминар рекомендован для 3-5 курсов.