Программирование с зависимыми типами на языке Idris
Курс
Курс посвящён различным аспектам программирования на языке Idris:
- типы как сущности первого класса, функции на типах;
- зависимые типы и зависимое сопоставление с образцом;
- приёмы доказательства равенств, разрешимости и тотальности;
- выражение отношений средствами зависимых типов;
- вычисление эффектов.
Для успешного прохождения курса желательны начальные навыки программирования на языке Haskell или другом функциональном языке программирования.
Страница курса на Computer Science Club
Лекции курса
10