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

Программирование с зависимыми типами на языке 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, Лекция ПОМИ РАН видео