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

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

Лекции

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

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

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

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

Лекция 5. System F

Лекция 6. System Fω

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

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

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

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

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

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

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

Ссылки

• B. C. Pierce - Types and Programming Languages (RU)

• M. H. Sørensen, P. Urzyczyn - Lectures on the Curry-Howard Isomorphism

• H. P. Barendregt - Lambda Calculi with Types

• H. Geuvers - Introduction to Type Theory

• D. Aspinall, M. Hofmann - Dependent Types

• J. Malakhovski - Brutal [Meta]Introduction to Dependent Types in Agda

• P. Wadler - Theorems for Free!

• F. Pottier, D. Rémy - The Essence of ML Type Inference

• 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

• D. Walker - Substructural Type Systems

• Д. Н. Москвин - Типы в языках программирования, 2015 год

• Д. Н. Москвин - Системы типизации лямбда-исчисления, 2011 год