Город: Санкт-Петербург Казань Язык: Русский English

Программирование с зависимыми типами на языке Idris
Санкт-Петербург / весна 2017, посмотреть все семестры

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

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

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

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

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

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

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

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

19 февраля 2017

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

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

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

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

13 февраля 2017

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

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

02 февраля 2017

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

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

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