Сайт в процессе наполнения. Архив всех прошедших курсов доступен на старой версии сайта по адресу old.compsciclub.ru
Город: Санкт-Петербург Казань Язык: Русский English

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


Запишитесь на курс, чтобы получать уведомления и иметь возможность сдавать домашние задания. Для записи требуется регистрация на сайте.
Перейти к регистрации Войти

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

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

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

Занятия

Дата Время Название Место Материалы
11.02.2017 17:20–18:50 Лекция 1 ПОМИ РАН Лекция Нет
11.02.2017 19:10–20:50 Лекция 2 ПОМИ РАН Лекция Нет
12.02.2017 11:15–12:45 Лекция 3 ПОМИ РАН Лекция Нет
12.02.2017 13:00–14:30 Лекция 4 ПОМИ РАН Лекция Нет
12.02.2017 15:30–17:00 Лекция 5 ПОМИ РАН Лекция Нет
18.02.2017 17:20–18:55 Лекция 6 ПОМИ РАН Лекция Нет
18.02.2017 19:15–20:50 Лекция 7 ПОМИ РАН Лекция Нет
19.02.2017 11:15–12:50 Лекция 8 ПОМИ РАН Лекция Нет
19.02.2017 13:00–14:30 Лекция 9 ПОМИ РАН Лекция Нет
19.02.2017 15:30–17:00 Лекция 10 ПОМИ РАН Лекция Нет