Мини-курс В.Н. Брагилевского: «Функциональное программирование с зависимыми типами на языке Idris»
На факультете компьютерных наук с 21 ноября по 1 декабря 2017 года пройдет мини-курс В.Н. Брагилевского: «Функциональное программирование с зависимыми типами на языке Idris».
Адрес: Кочновский пр-д, д. 3.
Расписание занятий:
- 21 ноября, вторник, 16:40–19:30, а. 219
- 23 ноября, четверг, 16:40–19:30, а. 219
- 27 ноября, понедельник, 16:40–19:30, а. 219
- 29 ноября, среда, 16:40–19:30, а. 219
- 1 декабря, пятница, 16:40–19:30, а. 300
Информация о курсе, где будут публиковаться слайды лекций и упражнения:
https://github.com/bravit/idris-cs-hse
Язык программирования Idris — это современный язык общего назначения, его первая версия была выпущена 1 апреля 2017 года. Он поддерживает функциональный стиль программирования и является наследником языка программирования Haskell, но в отличие от последнего реализует строгие вычисления и имеет более богатую систему типизации, а именно зависимые типы. Основная цель языка Idris состоит в том, чтобы применять возможности зависимых типов по более или менее точному специфицированию намерений разработчика программного обеспечения в практических задачах. Курс будет посвящён различным аспектам программирования на языке Idris, таким как функции на типах и зависимые типы, интерфейсы, выражение отношений между данными, представления, тотальность и верификация бесконечно работающих программ, управление состоянием. Также будут рассмотрены существенные для разработки корректного программного обеспечения элементы функционального программирования и теории типов.
Примерные темы лекций
- Введение в Idris, элементы функционального программирования.
- Теоретические основы верификации ПО средствами зависимых типов.
- Типы данных и ввод-вывод.
- Типы как сущности первого класса, функции на типах.
- Интерфейсы, модули и пространства имён.
- Выражение отношений на данных.
- Idris как система доказательства теорем.
- Тотальность и обработка бесконечных потоков данных.
- Типобезопасное управление состоянием.
- Конкурентное программирование.
Практическая часть
Слушателям будет предложено по ходу курса самостоятельно выполнять наборы упражнений (в закрытых репозиториях на github.com), а в конце курса выполнить финальный проект по разработке ПО на языке Idris с использованием зависимых типов.
Предварительные требования
Курс ориентирован на студентов второго-третьего годов бакалавриата и заинтересованных студентов магистратуры по компьютерным направлениям. От слушателей требуется уверенное владение любым императивным (объектно-ориентированным) языком программирования, желательно также хотя бы поверхностное знакомство с каким-либо функциональным языком программирования и базовыми понятиями математической логики.
Литература
- E. Brady. Type-driven Development with Idris. Manning Publishing, 2017.
- Документация по языку Idris. https://www.idris-lang.org/documentation/
О лекторе
Виталий Николаевич Брагилевский работает в Институте математики, механики и компьютерных наук Южного федерального университета (Ростов-на-Дону), где на протяжении десяти лет читает курсы по функциональному программированию, он ведёт активную деятельность по продвижению функционального программирования (языки Haskell и Idris) и теории языков программирования, а также является членом международного комитета по стандартизации языка программирования Haskell (Haskell 2020 Language Committee). В. Н. Брагилевский редактировал переводы на русский язык таких книг как «Изучай Haskell во имя добра» (М. Липовача) и «Чисто функциональные структуры данных» (К. Окасаки), а также участвовал в переводах книг «Жемчужины проектирования функциональных алгоритмов» (Р. Бёрд), «Параллельное и конкурентное программирование на языке Haskell» (С. Марлоу), «Введение в теорию языков программирования» (Ж. Довек и Ж.-Ж. Леви), он также сотрудничает с издательством Manning Publishing в качестве внешнего рецензента для книг по соответствующей тематике.