Анонс
Буду со следующего воскресенья (27.02.2011) читать в Computer Science клубе при ПОМИ РАН читать курс Системы типизации лямбда-исчисления.
Лекция 1. Система лямбда-исчисления без типов
Применение и абстракция. Свободные и связанные переменные. Комбинаторы. Функции нескольких переменных, каррирование. Подстановка, лемма подстановки. Бета-преобразование. Теорема о неподвижной точке, Y-комбинатор.
Лекция 2. Программирование в лямбда-исчислении и лямбда-определимость
Лямбда-исчисление как язык программирования. Булевы значения, пары. Числа Чёрча, операции над ними. Примитивная рекурсия. Списки. Лямбда-определимость и вычислимость по Тьюрингу. Неразрешимость бестипового лямбда-исчисления.
Лекция 3. Отношение редукции
Редексы. Одношаговая и многошаговая $\beta$-редукция, $\beta$-эквивалентность. $\beta$-нормальная форма. Редукционные графы. Теорема Чёрча-Россера. Следствия: редуцируемость к нормальной форме, единственность нормальной формы. Нормальная и аппликативные стратегии редукции. Теорема о нормализации.
Лекция 4. Просто типизированное лямбда-исчисление
Система $\lambda_{\rightarrow}$. Предтермы. Отношение типизации. Контексты. Правила типизации по Карри и по Чёрчу. Деревья вывода типов. Система минимальной пропозициональной логики. Соответствие Карри-Говарда. Леммы о контекстах. Типизируемость подтермов, нетипизируемые предтермы.
Лекция 5. Свойства просто типизированной системы
Лемма подстановки. Редукция субъекта. Незамкнутость относительно экспансии. Уникальность типов для типизации по Чёрчу. Связь между системами Карри и Черча. Вывод типов для $\lambda_{\rightarrow}$ в стиле Карри. Главный (наиболее общий) тип. Унификация. Алгоритм Хиндли-Милнера.
Дальше пока приблизительно:
Лекция 6. Слабая и сильная нормализация. Расширение систем константами.
Лекция 7. Полиморфная типизация. System F
Let-полиморфизм
Лекция 8. Параметричность. Свободные теоремы
Лекция 9 Операторы над типами. Зависимые типы
Лекция 10 Лямбда-куб. PTS
Лекция 11 Рекурсивные типы
Лекция 12 Рекурсивные типы
Литература:
LCWT
Henk Barendregt, Lambda calculi with types,
Handbook of logic in computer science (vol. 2), Oxford University Press, 1993
ITT
Herman Geuvers, Introduction to Type Theory
Alfa Lernet Summer school 2008, Uruguay
http://www.cs.ru.nl/H.Geuvers/Uruguay2008SummerSchool.html/
TAPL
Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002
http://www.cis.upenn.edu/~bcpierce/tapl
ATTAPL
Benjamin C. Pierce, editor. Advanced Topics in Types and Programming Languages,
MIT, 2005
ЛИСС
Х. Барендрегт, Ламбда-исчисление, его синтаксис и семантика,
М:Мир, 1985
Обратите внимание, что лекции будут некоторое время в Академическом университете, на Фонтанке - ремонт (подробности - по первой ссылке).
Лекция 1. Система лямбда-исчисления без типов
Применение и абстракция. Свободные и связанные переменные. Комбинаторы. Функции нескольких переменных, каррирование. Подстановка, лемма подстановки. Бета-преобразование. Теорема о неподвижной точке, Y-комбинатор.
Лекция 2. Программирование в лямбда-исчислении и лямбда-определимость
Лямбда-исчисление как язык программирования. Булевы значения, пары. Числа Чёрча, операции над ними. Примитивная рекурсия. Списки. Лямбда-определимость и вычислимость по Тьюрингу. Неразрешимость бестипового лямбда-исчисления.
Лекция 3. Отношение редукции
Редексы. Одношаговая и многошаговая $\beta$-редукция, $\beta$-эквивалентность. $\beta$-нормальная форма. Редукционные графы. Теорема Чёрча-Россера. Следствия: редуцируемость к нормальной форме, единственность нормальной формы. Нормальная и аппликативные стратегии редукции. Теорема о нормализации.
Лекция 4. Просто типизированное лямбда-исчисление
Система $\lambda_{\rightarrow}$. Предтермы. Отношение типизации. Контексты. Правила типизации по Карри и по Чёрчу. Деревья вывода типов. Система минимальной пропозициональной логики. Соответствие Карри-Говарда. Леммы о контекстах. Типизируемость подтермов, нетипизируемые предтермы.
Лекция 5. Свойства просто типизированной системы
Лемма подстановки. Редукция субъекта. Незамкнутость относительно экспансии. Уникальность типов для типизации по Чёрчу. Связь между системами Карри и Черча. Вывод типов для $\lambda_{\rightarrow}$ в стиле Карри. Главный (наиболее общий) тип. Унификация. Алгоритм Хиндли-Милнера.
Дальше пока приблизительно:
Лекция 6. Слабая и сильная нормализация. Расширение систем константами.
Лекция 7. Полиморфная типизация. System F
Let-полиморфизм
Лекция 8. Параметричность. Свободные теоремы
Лекция 9 Операторы над типами. Зависимые типы
Лекция 10 Лямбда-куб. PTS
Лекция 11 Рекурсивные типы
Лекция 12 Рекурсивные типы
Литература:
LCWT
Henk Barendregt, Lambda calculi with types,
Handbook of logic in computer science (vol. 2), Oxford University Press, 1993
ITT
Herman Geuvers, Introduction to Type Theory
Alfa Lernet Summer school 2008, Uruguay
http://www.cs.ru.nl/H.Geuvers/Uruguay2008SummerSchool.html/
TAPL
Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002
http://www.cis.upenn.edu/~bcpierce/tapl
ATTAPL
Benjamin C. Pierce, editor. Advanced Topics in Types and Programming Languages,
MIT, 2005
ЛИСС
Х. Барендрегт, Ламбда-исчисление, его синтаксис и семантика,
М:Мир, 1985
Обратите внимание, что лекции будут некоторое время в Академическом университете, на Фонтанке - ремонт (подробности - по первой ссылке).
no subject
no subject
no subject
no subject
no subject
no subject
no subject
no subject
я не очень уверен насчёт публичного статуса перевода - не то чтобы я был борцом за дело копирайта, но это дело ребят его прояснить
no subject
no subject
no subject
no subject
у них, вроде, переговоры с издательством и сейчас не знаю, насколько лишняя публичность им нужна
no subject
no subject
no subject
no subject
no subject
ну и понятно, что в ПОМИ традиционный академический формат. Практические занятия не предусмотрены, их качественная организация, кстати, не самое простое дело.
no subject
Кстати, я в CS-клубе всё с удовольствием слушаю. Жалко, в этом семестре воскресенье полностью пересекается с физматклубом, а ваши лекции, судя по всему только по воскресеньям...
no subject
посмотрим, эта часть ещё в работе
no subject
no subject
А ты умеешь? А то тут на Coq'еров проскакивал некоторый спрос.
no subject
no subject
no subject
no subject
в литературу я бы еще понапихал http://adam.chlipala.net/cpdt/, для развития. Ну и Cardelli тоже, хотя Пирс его покрывает
no subject
А вторая, Certified Programming with Dependent Types, это, конечно, для отдельного, специального курса.
no subject
кто может прийти?
что надо что бы прийти?
no subject
http://logic.pdmi.ras.ru/csclub/faq
только лекции будут не на Фонтанке, а в Академическом университете
http://logic.pdmi.ras.ru/csclub/node/1084
no subject
no subject