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

Programming with Dependent Types in Idris
Saint Petersburg / spring 2017, посмотреть все семестры

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

Курс посвящён различным аспектам программирования на языке Idris:

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

Для успешного прохождения курса желательны начальные навыки программирования на языке Haskell или другом функциональном языке программирования.

Упражнения по курсу будут публиковаться в закрытом репозитории, поэтому прошу слушателей курса, желающих выполнять упражнения, указать в своём профиле аккаунт на GitHub.

Date and time Class|Name Venue|short Materials
11 February
17:20–18:50
Лекция 1. Верификация ПО, соответствие Карри-Ховарда и зависимые типы, Lecture ПОМИ РАН slides,  video
11 February
19:10–20:50
Лекция 2. Интерактивная разработка через типы, Lecture ПОМИ РАН slides,  video
12 February
11:15–12:45
Лекция 3. Типы данных и ввод-вывод, Lecture ПОМИ РАН slides,  video
12 February
13:00–14:30
Лекция 4. Типы как сущности первого класса, функции на типах, Lecture ПОМИ РАН slides,  video
12 February
15:30–17:00
Лекция 5. Интерфейсы, модули и пространства имён, Lecture ПОМИ РАН slides,  video
18 February
17:20–18:55
Лекция 6. Выражение отношений на данных средствами зависимых типов, Lecture ПОМИ РАН slides,  video
18 February
19:15–20:50
Лекция 7. Доказательство теорем, Lecture ПОМИ РАН video
19 February
11:15–12:50
Лекция 8. Вычисления с эффектами, Lecture ПОМИ РАН slides,  video
19 February
13:00–14:30
Лекция 9. Верификация протоколов на типах и определение EDSL, Lecture ПОМИ РАН slides,  videofiles
19 February
15:30–17:00
Лекция 10. Представления и конструкция with, Lecture ПОМИ РАН video