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

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

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

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

Дата и время Название Место Материалы
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, лекция ПОМИ РАН Нет
19 февраля
15:30–17:00
Лекция 10, лекция ПОМИ РАН Нет