Просто типизированное лямбда-исчисление

Четверг, 01 февраля 2018
НГУ, ауд. 2128, НГУ, новый корпус

Слайды с лекции

func_prog_lecture_010218.pdf

Описание

Роль типов в языках программирования. Предтермы. Утверждения о типизации. Контексты. Правила типизации по Карри и по Чёрчу. Деревья вывода типов. Свойства типизированного лямбда-исчисления. Связь между системами Карри и Чёрча. Проблемы разрешимости. Сильная и слабая нормализация. Соответствие Карри-Говарда.