Математические модели вычислений
Лекции читают:
- д.ф.-м.н., проф. Валерий Александрович Васенин,
- к.ф.-м.н., с.н.с. Максим Александрович Кривчиков
В осеннем семестре рассматриваются фундаментальные вопросы формальных моделей вычислений и утверждения, ограничивающие применимость методов формальной верификации. Слушатели получат представление о теоретических основаниях дедуктивных методов формальной верификации программ на примере разновидностей типизированного λ-исчисления.
В 2023 году спецкурс читается дистанционно, первая лекция 15 сентября. Запись для слушателей курса по email: maxim.krivchikov@gmail.com.
В весеннем семестре традиционно читается продолжение курса на английском языке. Страница второй части курса: http://maxxk.github.io/programming-languages/
Презентации
Для просмотра презентаций в дисплейных классах нужно использовать Firefox с включенным JavaScript (кнопка «Настройка» → «Разрешить все» в правой нижней части окна).
Введение (2023-09-15)
Обзор курса. Предпосылки к задаче формальной верификации, актуальность. Современные методы верификации программ (рецензирование, тестирование, статический анализ, формальная верификация) и их интеграция в процессы разработки.
Entscheidungsproblem (проблема разрешения). Машина Тьюринга. Конечные автоматы и формальные языки. (2023-09-22)
Альтернативные модели вычислений. (2023-09-29)
Формальные системы. (2022-10-07, 2022-10-14)
Введение в верификацию с использованием методов Model Checking. (2022-10-21)
Нормальные алгорифмы Маркова. Нетипизированное λ-исчисление. λ-исчисление с простыми типами.
(2022-10-28, 2022-11-11)
Алгоритмы проверки типов и свойство сильной нормализации (2022-11-11)
Расширения типизированного λ-исчисления. Полиморфное λ-исчисление. (2022-11-18)
Примеры исходного кода проверки типов, вывода типов и вывода термов с лекции: https://github.com/maxxk/formal-models/tree/gh-pages/code.
Дополнительные задания:
- Добавить проверку и вывод типов для λ-исчисления с простыми типами с произведением и суммой типов.
- Добавить вывод термов для λ-исчисления с простыми типами с произведением и суммой типов и продемонстрировать автоматический вывод аксиом исчисления высказываний (без отрицания).
Дополнительные материалы:
https://crypto.stanford.edu/~blynn/lambda/systemf.html
https://www.sciencedirect.com/science/article/pii/S0168007298000475
Расширения типизированного λ-исчисления. Конструкторы типов и зависимые типы. (2020-12-02, 2020-12-09)
Индуктивные и коиндуктивные типы. Работа в среде Coq. (2020-12-16)
Дополнительный материал для самостоятельного ознакомления, который не вошёл в программу в 2020 году:
Гомотопическая теория типов.
https://github.com/HoTT/book/wiki/Nightly-Builds
Самоинтерпретация системы F_ω?
http://compilers.cs.ucla.edu/popl16/
Список вопросов
Список вопросов к экзамену доступен по ссылке.