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

Системы типизации лямбда-исчисления
Санкт-Петербург / весна 2011, посмотреть все семестры

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

Современные функциональные языки программирования, такие как Haskell, наследники ML (SML, Ocaml, F#), Agda2 и т.п., обладают весьма богатыми и сложными системами типов. Несмотря на такое разнообразие, эти системы имеют в своей основе хорошо проработанную формальную теорию типизированных лямбда-исчислений.

В рамках курса рассматриваются различные системы типизации лямбда-исчисления. Понятие типа вводится на примере просто типизированного чистого лямбда-исчисления. Исследуются два основных подхода к типизации лямбда-исчисления: в стиле Карри и в стиле Чёрча. Обсуждаются следующие системы: полиморфные типы (System F), операторы над типами, полиморфизм высших порядков, зависимые типы, рекурсивные типы. Для изучаемых систем исследуются проблемы проверки, присваивания (синтеза) и населенности типов. Обсуждается связь между различными логическими системами и системами типов.

Решения домашних заданий можно присылать на адрес dmoskvin@gmail.com

Дата и время Занятие Место Материалы
27 февраля
11:15–12:50
Система лямбда-исчисления без типов, Лекция ПОМИ РАН слайды,  видео
27 февраля
13:00–14:35
Программирование в лямбда-исчислении и лямбда-определимость, Лекция ПОМИ РАН слайды,  видео
06 марта
11:15–12:50
Отношение редукции, Лекция ПОМИ РАН слайды,  видео
06 марта
13:00–14:35
Просто типизированное лямбда-исчисление, Лекция ПОМИ РАН слайды,  видео
13 марта
11:15–12:50
Свойства просто типизированной системы, Лекция ПОМИ РАН слайды,  видео
13 марта
13:00–14:35
Просто типизированная система: разрешимость, нормализация, расширения, Лекция ПОМИ РАН слайды,  видео
27 марта
11:15–12:50
Полиморфные системы типов, Лекция ПОМИ РАН слайды,  видео
27 марта
13:00–14:35
Полиморфные системы: логическая интерпретация и программирование, Лекция ПОМИ РАН слайды,  видео
15 мая
11:15–12:50
Лямбда-куб Барендрегта, Лекция ПОМИ РАН слайды
15 мая
13:00–14:35
Лямбда-куб и логические системы, Лекция ПОМИ РАН слайды
22 мая
11:15–12:50
Чистые системы типов, Лекция ПОМИ РАН слайды
22 мая
13:00–14:35
Рекурсивные типы и типы-пересечения, Лекция ПОМИ РАН слайды