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

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

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

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

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