You are currently at the new webpage of the Club. The list of all courses of the Club is available at the old page: old.compsciclub.ru
City: Saint-Petersburg Kazan Language: Русский English

Programming with Dependent Types in Idris
Spring 2017, посмотреть все семестры

Enroll in the course to get notifications and to be able to submit home assignments.
Register to enroll now Login

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

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

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

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

Date and time Class|Name Venue|short Materials
11 February
17:20–18:50
Лекция 1. Верификация ПО, соответствие Карри-Ховарда и зависимые типы, lecture ПОМИ РАН slidesvideo
11 February
19:10–20:50
Лекция 2. Интерактивная разработка через типы, lecture ПОМИ РАН slidesvideo
12 February
11:15–12:45
Лекция 3. Типы данных и ввод-вывод, lecture ПОМИ РАН slidesvideo
12 February
13:00–14:30
Лекция 4. Типы как сущности первого класса, функции на типах, lecture ПОМИ РАН slidesvideo
12 February
15:30–17:00
Лекция 5. Интерфейсы, модули и пространства имён, lecture ПОМИ РАН slidesvideo
18 February
17:20–18:55
Лекция 6. Выражение отношений на данных средствами зависимых типов, lecture ПОМИ РАН slidesvideo
18 February
19:15–20:50
Лекция 7. Доказательство теорем, lecture ПОМИ РАН video
19 February
11:15–12:50
Лекция 8. Вычисления с эффектами, lecture ПОМИ РАН slidesvideo
19 February
13:00–14:30
Лекция 9. Верификация протоколов на типах и определение EDSL, lecture ПОМИ РАН slidesvideo, files
19 February
15:30–17:00
Лекция 10. Представления и конструкция with, lecture ПОМИ РАН video
07 March 2017

Видео лекций доступны

На сайте опубликованы видео-записи лекций.

19 February 2017

Второй набор упражнений и экзаменационный проект

В репозитории с заданиями опубликованы ссылка для создания репозитория с вторым набором упражнений и описание экзаменационного проекта.

Оба набора упражнений и экзаменационный проект должны быть выполнены до 09.04.2017. После завершения работы необходимо выслать мне адреса всех репозиториев (соответствующие правила и мои контакты приведены на слайдах первой лекции) и договориться об онлайн-сдаче экзаменационного проекта.

В.Н. Брагилевский

13 February 2017

Первый набор упражнений

Слушателям курса, указавшим в своём профиле GitHub-аккаунт, стал доступен репозиторий со ссылкой на первый набор упражнений. В случае проблем с доступом к упражнениям необходимо связаться с преподавателем (все контакты имеются на слайдах к первой лекции) и сообщить имя своего аккаунта на GitHub.

02 February 2017

GitHub-аккаунты в профиле

Уважаемые слушатели!

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