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

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

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

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