TAPL 5SE весна 2021 — различия между версиями
Moskvin (обсуждение | вклад) (→Слайды) |
Moskvin (обсуждение | вклад) (→Слайды) |
||
(не показана 1 промежуточная версия этого же участника) | |||
Строка 37: | Строка 37: | ||
[[Медиа:tapl102021.pdf|Лекция 10. Зависимые типы: система λP]] | [[Медиа:tapl102021.pdf|Лекция 10. Зависимые типы: система λP]] | ||
− | + | 12.05.2021 (ср) 13:45-15:45, online | |
[[Медиа:tapl112021.pdf|Лекция 11. λ-куб и чистые системы типов]] | [[Медиа:tapl112021.pdf|Лекция 11. λ-куб и чистые системы типов]] | ||
− | + | 19.05.2021 (ср) 13:45-15:45, online | |
[[Медиа:tapl122021.pdf|Лекция 12. Логические системы]] | [[Медиа:tapl122021.pdf|Лекция 12. Логические системы]] | ||
− | + | 26.05.2021 (ср) 13:45-15:45, online | |
=== Литература === | === Литература === |
Текущая версия на 11:02, 20 апреля 2021
Содержание
Лекции
Преподаватель: Москвин Денис Николаевич (λxy.dmoskvinxgmailycom)@.
Пожалуйста, указывайте в теме письма TAPL2021.
Слайды
Лекция 1. Язык арифметических выражений 10.02.2021 (ср) 13:40-15:40, online
Лекция 2. Простые типы 17.02.2021 (ср) 13:45-15:45, online
Лекция 3. Простые расширения 03.03.2021 (ср) 13:45-15:45, online
Лекция 4. Обитаемость простых типов 10.03.2021 (ср) 13:45-15:45, online
Лекция 5. Нормализация для простой системы и типы-пересечения 17.03.2021 (ср) 13:45-15:45, online
Лекция 6. Подтипы 24.03.2021 (ср) 13:45-15:45, online
Лекция 7. Полиморфные типы: система λ2 (System F) 31.03.2021 (ср) 13:45-15:45, online
Практика. Полиморфные типы 07.04.2021 (ср) 13:45-15:45, online
Лекция 8. Экзистенциальные типы 14.04.2021 (ср) 13:45-15:45, online
Лекция 9. Операторы над типами: система λω 21.04.2021 (ср) 13:45-15:45, online
Лекция 10. Зависимые типы: система λP 12.05.2021 (ср) 13:45-15:45, online
Лекция 11. λ-куб и чистые системы типов 19.05.2021 (ср) 13:45-15:45, online
Лекция 12. Логические системы 26.05.2021 (ср) 13:45-15:45, online
Литература
Книги и статьи перечислены в убывающем порядке важности для изучения курса.
Пирс Б. Типы в языках программирования. — Лямбда пресс, Добросвет, 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.
Практика
Преподаватель: Москвин Денис Николаевич (λxy.dmoskvinxgmailycom)@.
Пожалуйста, указывайте в теме письма TAPL2021.
Текущая успеваемость
Для образовательных программ с 5-бальной системой оценок проценты переводятся в баллы следующей функцией
score :: Int -> Int score proc | proc < 51 = 0 | proc > 98 = 5 | otherwise = (proc - 51) `div` 8
Домашние задания на stepik.org
Для выполнения домашних заданий следует:
Если вы ранее не обучались на Stepik, зарегистрироваться на Stepik. Настоятельная просьба - указать идентификационные данные, позволяющие опознавать вас без сложных исследований.
Перейти по ссылке-приглашению на курс
Модули с текущим ДЗ будут становиться доступными по мере прохождения курса, дедлайны будут видны там же.