Программирование с зависимыми типами на языке Idris
Весна 2017, посмотреть все семестры

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

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

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

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

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