Город: Тест Санкт-Петербург Новосибирск Казань Язык: Русский English

Введение в язык формальной верификации Coq
Санкт-Петербург / осень 2019, посмотреть все семестры

Запишитесь на курс, чтобы получать уведомления и иметь возможность сдавать домашние задания. Для записи требуется регистрация на сайте.
Перейти к регистрации Войти

В первой части мы обсудим формальные доказательства и Coq в общем, разберемся для чего он нужен, где применяется, его место среди других инструментов формальной верификации, затронем экосистему Coq, а также рассмотрим методы связи верифицированных программ и исполняемого кода, такие как экстракция и эмбединг.

Во второй части посмотрим на многочисленных примерах на особенности Coq как языка программирования. В процессе обсудим слабую/сильную нормализацию, зависимые типы, тактики, тотальность, строгую позитивность, иерархию вселенных типов, непредикативность, различия между Type и Prop, экстракцию.

Дата и время Занятие Место Материалы
21 сентября
15:30–17:00
Лекция 1, Лекция ПОМИ РАН видео
22 сентября
13:10–14:40
Лекция 2, Лекция ПОМИ РАН видео