С 6 октября начинает работу специальный курс для студентов 2–6 курса и магистрантов механико-математического факультета МГУ имени М. В. Ломоносова
Формальные модели вычислений
Лекции читают:
- д.ф.-м.н., проф. Валерий Александрович Васенин,
- н.с. Максим Александрович Кривчиков
В осеннем семестре рассматриваются фундаментальные вопросы формальных моделей вычислений и утверждения, ограничивающие применимость методов формальной верификации. Слушатели получат представление о теоретических основаниях дедуктивных методов формальной верификации программ на примере разновидностей типизированного λ-исчисления.
В весеннем семестре будет читаться продолжение курса, в котором будут рассмотрены практические аспекты описания формальной семантики и формальной верификации функциональных свойств программ.
Время проведения: вторник, 16:55–18:20, ауд. 1307.
Курс входит в число обязательных кафедральных дисциплин для студентов 5 курса кафедры вычислительной математики.
На настоящем сайте будут выкладываться материалы к занятиям.
Пройдите анонимный опрос — обратную связь по итогам курса.
Материалы к занятиям
6.10.2015 Вводное занятие (презентация — pdf)
13.10.2015 Фундаментальные модели вычислений (презентация — pdf)
27.10.2015 Формальные системы (презентация — pdf)
3.11.2015 Model checking (презентация — pdf)
10.11.2015 λ-исчисление с простыми типами (презентация — html) (презентация — pdf)
17.11.2015 Расширения типизированного λ-исчисления (презентация — html) (презентация — pdf)
24.11.2015 Исчисление конструкций (презентация — html) (презентация — pdf)
01.12.2015 Индуктивные и коиндуктивные типы (презентация — html) (презентация — pdf)
08.12.2015 Гомотопическая теория типов (презентация — html) (презентация — pdf)
Литература
(предварительный список)
Основная литература:
- Б. Пирс. Типы и языки программирования. М.: Лямбда-пресс: Добросвет. 2011.
- A. Chlipala. Certified Programming With Dependent Types. MIT Press. 2013.
- Univalent Foundations Program. Homotopy Type Theory. 2012.
- S. Thompson. Type Theory and Functional Programming. Addison-Wesley, 1991.
- А.Б. Угольников (ред.). Конспект лекций О.Б.Лупанова по курсу “Введение в математическую логику”, 2007.
- H. Barendregt. Introduction to generalized type systems. J.Funct.Program, (2):125-154, 1991.
Дополнительная литература (библиографический обзор курса, ссылки на оригинальные публикации, содержащие рассматриваемые в курсе результаты):
- В.А. Васенин, М.А. Кривчиков. Формальные модели программ и языков программирования. Часть 1. Библиографический обзор 1930—1989 гг. Программная инженерия, (5):10–19, 2015.
- В.А. Васенин, М.А. Кривчиков. Формальные модели программ и языков программирования. Часть 2. Современное состояние исследований. Программная инженерия, (6):24–33, 2015.
Перечень ресурсов информационно-телекоммуникационной сети «Интернет»:
- Обновляемая страница курса: http://maxxk.github.io/formal-models-2015/
- М.Р. Пентус. Введение в математическую логику. Конспект лекций на механико-математическом факультете МГУ, весна 2006. http://lpcs.math.msu.su/~pentus/ftp/mehmat/vmlk06le.pdf
Электронные версии книг из списка основной литературы курса:
- A. Chlipala. Certified Programming With Dependent Types. http://adam.chlipala.net/cpdt/
- Univalent Foundations Program. Homotopy Type Theory. http://homotopytypetheory.org/book/
- S. Thompson. Type Theory and Functional Programming. http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/
Дополнительные ссылки на ресурсы информационно-телекоммуникационной сети Интернет приведены на обновляемой странице курса в материалах лекций.