Денис Москвин
К.ф.-м.н., доцент СПбТЭИ и СпбИВЭСЭП, преподаёт математику и программирование, область научных интересов: функциональные языки программирования и их с
Системы типизации лямбда-исчисления
Время проведения
Начало курса по мере набора группы
Длительность курса
24 часа
Стоимость
Бесплатно
Описание
Современные функциональные языки программирования, такие как Haskell, наследники ML (SML, Ocaml, F#), Agda2 и т.п., обладают весьма богатыми и сложными системами типов. Несмотря на такое разнообразие, эти системы имеют в своей основе хорошо проработанную формальную теорию типизированных лямбда-исчислений.
Форма проведения
В рамках курса рассматриваются различные системы типизации лямбда-исчисления. Понятие типа вводится на примере просто типизированного чистого лямбда-исчисления. Исследуются два основных подхода к типизации лямбда-исчисления: в стиле Карри и в стиле Чёрча. Обсуждаются следующие системы: полиморфные типы (System F), операторы над типами, полиморфизм высших порядков, зависимые типы, рекурсивные типы. Для изучаемых систем исследуются проблемы проверки, присваивания (синтеза) и населенности типов. Обсуждается связь между различными логическими системами и системами типов.
Преподаватель
Организатор
Computer Science клуб
Основная цель — предоставить студентам Санкт–Петербурга возможность получить образование в области Theoretical Computer Science.
Курс добавлен
пользователем kirpich
Подробнее о курсе:
http://logic.pdmi.ras.ru/csclub/courses/systemsoftypedlambdacalculi
Место проведения занятий:
http://logic.pdmi.ras.ru/csclub/node/1084
Комментарии