City: Test Saint Petersburg Novosibirsk Kazan Language: Русский English

Introduction to Coq
Saint Petersburg / autumn 2019, посмотреть все семестры

Enroll in the course to get notifications and to be able to submit home assignments.
Register to enroll now Login

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

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

Date and time Class|Name Venue|short Materials
21 September
15:30–17:00
Лекция 1, Lecture ПОМИ РАН video
22 September
13:10–14:40
Лекция 2, Lecture ПОМИ РАН video