Типы в языках программирования, 5 курс, 2 семестр, 2016/17

Преподаватель -- Елагин Кирилл

Лекции

Лекция 1. Синтакс и семантики

Лекция 2. Простое типизированное лямбдя-исчисление

Лекция 3. Нормализация

Лекция 4. АТД и рекурсивные типы

Лекция 5. System F

Лекция 6. System Fω

Лекция 7. Зависимые типы

Лекция 8. Чистые системы типов

Лекция 9. Проверка типов

Лекция 10. Катаморфизмы

Лекция 11. Подтипы

Лекция 12. Экзистенциальные типы

Лекция 13. Обзор: зипперы, типы-пересечения, субструктурные логики

Ссылки

• Б. Пирс - Типы в языках программирования
• M. H. Sørensen, P. Urzyczyn - Lectures on the Curry-Howard Isomorphism
• J. Malakhovski - Brutal [Meta]Introduction to Dependent Types in Agda
• E Meijer, M. Fokkinga, R. Paterson - Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire
• C. McBride - The Derivative of a Regular Type is its Type of One-Hole Contexts