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

Свойства просто типизированной системы
Системы типизации лямбда-исчисления

Что: Лекция
Когда: Воскресенье, 13 марта 2011, 11:15–12:50
Где: ПОМИ РАН
Слайды: systemsoftypedlambdacalculi_lecture_130311.pdf

Описание

Леммы о контекстах. Типизируемость подтермов, нетипизируемые предтермы. Лемма подстановки. Теорема о редукции субъекта. Незамкнутость относительно экспансии. Уникальность типов для типизации по Чёрчу. Связь между системами Карри и Черча. Главный (наиболее общий) тип для \( \lambda_{\rightarrow} \) в стиле Карри. Свойства подстановки. Унификация. Алгоритм Хиндли-Милнера.

Видео