City: Saint Petersburg Novosibirsk Kazan Language: Русский English

Systems of typed lambda calculi
Saint Petersburg / spring 2011, посмотреть все семестры

Enroll in the course to get notifications and to be able to submit home assignments.
Register to enroll now Login

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.

Date and time Class|Name Venue|short Materials
27 February
11:15–12:50
Система лямбда-исчисления без типов, Lecture ПОМИ РАН slides,  video
27 February
13:00–14:35
Программирование в лямбда-исчислении и лямбда-определимость, Lecture ПОМИ РАН slides,  video
06 March
11:15–12:50
Отношение редукции, Lecture ПОМИ РАН slides,  video
06 March
13:00–14:35
Просто типизированное лямбда-исчисление, Lecture ПОМИ РАН slides,  video
13 March
11:15–12:50
Свойства просто типизированной системы, Lecture ПОМИ РАН slides,  video
13 March
13:00–14:35
Просто типизированная система: разрешимость, нормализация, расширения, Lecture ПОМИ РАН slides,  video
27 March
11:15–12:50
Полиморфные системы типов, Lecture ПОМИ РАН slides,  video
27 March
13:00–14:35
Полиморфные системы: логическая интерпретация и программирование, Lecture ПОМИ РАН slides,  video
15 May
11:15–12:50
Лямбда-куб Барендрегта, Lecture ПОМИ РАН slides
15 May
13:00–14:35
Лямбда-куб и логические системы, Lecture ПОМИ РАН slides
22 May
11:15–12:50
Чистые системы типов, Lecture ПОМИ РАН slides
22 May
13:00–14:35
Рекурсивные типы и типы-пересечения, Lecture ПОМИ РАН slides