TAPL весна 2022

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

Лекции

Преподаватель: Москвин Денис Николаевич (λxy.dmoskvinxgmailycom)@.

Пожалуйста, указывайте в теме письма TAPL2022.

Слайды

Лекция 0. Введение 09.02.2022 (ср) 15:00-17:00, online

Лекция 1. Язык арифметических выражений 16.02.2022 (ср) 15:00-17:00, Таймс, 204

Лекция 2. Простые типы 23.02.2022 (ср) 15:00-17:00, online

Лекция 3. Простые расширения 02.03.2022 (ср) 15:00-17:00, Таймс, 204

Лекция 4. Обитаемость простых типов 09.03.2022 (ср) 15:00-17:00, online

Лекция 5. Нормализация для простой системы и типы-пересечения 16.03.2022 (ср) 15:00-17:00, Таймс, 204

Лекция 6. Подтипы 23.03.2022 (ср) 15:00-17:00, Таймс, 204

Лекция 7. Полиморфные типы: система λ2 (System F) 30.03.2022 (ср) 15:00-17:00, Таймс, 204

Практика. Полиморфные типы 06.04.2022 (ср) 15:00-17:00, Таймс, 204

Лекция 8. Экзистенциальные типы 13.04.2022 (ср) 15:00-17:00, Таймс, 204

Лекция 9. Операторы над типами: система λω 20.04.2022 (ср) 15:00-17:00, Таймс, 204

Лекция 10. Зависимые типы: система λP 27.04.2022 (ср) 15:00-17:00, Таймс, 204

Лекция 11. λ-куб и чистые системы типов 18.05.2022 (ср) 15:00-17:00, Таймс, 204

Лекция 12. Логические системы 25.05.2022 (ср) 15:00-17:00, Таймс, 204

Литература

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

Пирс Б. Типы в языках программирования. — Лямбда пресс, Добросвет, 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)@.

Пожалуйста, указывайте в теме письма TAPL2022.

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

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

Для образовательных программ с бинарной шкалой оценок (зачет/незачет) для получения зачета необходимо набрать не меньше 78%.

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

score5 :: Int -> Int
score5 proc
  | proc < 60 = 0
  | proc > 95 = 5
  | otherwise = (proc - 60) `div` 6

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

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

Для образовательных программ со шкалой оценок ECTS (A-F) проценты переводятся в баллы функцией

scoreAF :: Int -> Char
scoreAF proc
  | s10 < 4   = 'F'
  | s10 > 8   = 'A'
  | otherwise = chr (73 - s10)
 where s10 = score10 proc

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

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

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

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

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