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

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

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

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

Страница курса на Computer Science Club