Типы в языках программирования 3 модуль 2019

Материал из CSC Wiki
Перейти к:навигация, поиск

Лекции

Преподаватель: Москвин Денис Николаевич dmoskvin@gmail.com

Слайды

Лекция 1. Язык арифметических выражений 05.02.2019 (вт)

Лекция 2. Простые типы 05.02.2019 (вт)

Лекция 3. Простые расширения 12.02.2019 (вт)

Лекция 4. Обитаемость простых типов 12.02.2019 (вт)

Лекция 5. Нормализация для простой системы 19.02.2019 (вт)

Лекция 6. Подтипы 19.02.2019 (вт)

Лекция 7. Полиморфные типы: система λ2 (System F) 26.02.2019 (вт)

Лекция 8. Экзистенциальные типы 05.03.2019 (вт)

Лекция 9. Операторы над типами: система λω 05.03.2019 (вт)

Лекция 10. Зависимые типы: система λP 12.03.2019 (вт)

Лекция 11. λ-куб и чистые системы типов 12.03.2019 (вт)

Лекция 12. Логические системы 19.03.2019 (вт)

Лекция 13. Типы-пересечения 19.03.2019 (вт)


Литература

Книги и статьи перечислены в убывающем порядке важности для изучения курса.

Пирс Б. Типы в языках программирования. — Лямбда пресс, Добросвет, 2012. — 656 c.

Hindley J. R. Basic simple type theory. — Cambridge University Press, 1997. — 186 pp.

Sorensen M. H., Urzyczyn P. Lectures on the Curry-Howard Isomorphism. — Elsevier, 2006. — 442 pp.

Barendregt H. Lambda calculi with types. — Handbook of logic in computer science (vol. 2), Oxford University Press, 1993. — 194 pp.

Barendregt H., Dekkers W., Statman R. Lambda Calculus with Types. — Cambridge University Press, 2013. — xxii + 833 pp.

Hindley J. R., Seldin J. P. Lambda-Calculus and Combinators, an Introduction. — Cambridge University Press, 2008. — xi + 345 pp.

Pierce B. C., ed. Advanced Topics in Types and Programming Languages. — MIT Press, 2005. — xiii + 574 pp. — xxii + 833 pp.

Барендрегт Х. Ламбда-исчисление, его синтаксис и семантика. М.:Мир. — 1985. — 606 с.

Nederpelt R, Geuvers H. Type Theory and Formal Proof: An Introduction. — Cambridge University Press, 2014. — 436 pp.

Практика

Преподаватель: Москвин Денис Николаевич dmoskvin@gmail.com

Текущая успеваемость

гугл-табличка успеваемости

Для образовательных программ с 10-бальной системой оценок проценты переводятся в баллы следующей функцией

score :: Int -> Int
score proc
  | proc < 66 = 0
  | proc > 96 = 10
  | otherwise = (proc - 66) `div` 3

Домашние задания на stepik.org

Для выполнения домашних заданий следует:

Если вы ранее не обучались на Stepik, зарегистрироваться на Stepik. Настоятельная просьба - указать идентификационные данные, позволяющие опознавать вас без сложных исследований.

Перейти по ссылке-приглашению на курс

Модули с текущим ДЗ будут становиться доступными по мере прохождения курса, дедлайны будут видны там же.