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

Русскоязычный курс от Computer Science Club, посвященный базовым аспектам программирования на языке Idris. Курс записан в 2017 году, лектор — Виталий Брагилевский.

В курсе рассматриваются следующие темы:

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

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