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

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

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

Modern functional programming languages such as Haskell, ML (and its successors - SML, Ocaml, F#), Agda2, etc, are equipped with rather rich and complex type systems. Despite this diversity, these systems are based on strong foundation of formal theory of typed lambda calculi.

The course is dedicated to the different systems of typed lambda calculi. The concept of a type is introduced for the pure simply typed lambda-calculus. The Curry-style and Church-style approaches to a typed lambda calculus are examined. The following systems will be discussed: polymorphic types (system F), type operators, higher-order polymorphism, dependent types, recursive types. For these systems the problems of type checking, type assignment (synthesis) and type inhabitation are examined. The correspondence between different logical and type systems is discussed.

Дата и время Название Место Материалы
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
Рекурсивные типы и типы-пересечения, лекция ПОМИ РАН слайды