Функциональное программирование с зависимыми типами на языке 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

Расписание для календаря

Темы лекций

1. Введение в Idris, элементы функционального программирования (примеры).
2. Теоретические основы верификации ПО средствами зависимых типов (примеры).
3. Типы данных и ввод-вывод (примеры).
4. Типы как сущности первого класса, функции на типах (примеры).
5. Интерфейсы, модули и пространства имён (примеры).
6. Выражение отношений на данных (примеры).
7. Idris как система доказательства теорем (примеры).
8. Тотальность и представления (примеры). 9-10. Бесконечные потоки данных и процессы, конечные автоматы и верификация протоколов, компиляция кода на Idris (примеры).

Предварительные требования

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

Литература

1. E. Brady. Type-driven Development with Idris. Manning Publications, 2017.
2. Документация по языку Idris. https://www.idris-lang.org/documentation/