Просмотр исходного текста страницы TAPL 5SE весна 2021

== Лекции ==
Преподаватель: Москвин Денис Николаевич <code>(λxy.dmoskvinxgmailycom)@.</code>

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

=== Слайды ===

[[Медиа:Tapl012021.pdf|Лекция 1. Язык арифметических выражений]]
10.02.2021 (ср) 13:40-15:40, online

[[Медиа:tapl022021.pdf|Лекция 2. Простые типы]] 
17.02.2021 (ср) 13:45-15:45, online

[[Медиа:tapl032021.pdf|Лекция 3. Простые расширения]] 
03.03.2021 (ср) 13:45-15:45, online

[[Медиа:tapl042021.pdf|Лекция 4. Обитаемость простых типов]] 
10.03.2021 (ср) 13:45-15:45, online

[[Медиа:tapl052021.pdf|Лекция 5. Нормализация для простой системы и типы-пересечения]] 
17.03.2021 (ср) 13:45-15:45, online

[[Медиа:tapl062021.pdf|Лекция 6. Подтипы]] 
24.03.2021 (ср) 13:45-15:45, online

[[Медиа:tapl072021.pdf|Лекция 7. Полиморфные типы: система λ2 (System F)]] 
31.03.2021 (ср) 13:45-15:45, online

[[Медиа:tapl072021pr.pdf|Практика. Полиморфные типы]] 
07.04.2021 (ср) 13:45-15:45, online

[[Медиа:tapl082021.pdf|Лекция 8. Экзистенциальные типы]] 
14.04.2021 (ср) 13:45-15:45, online

[[Медиа:tapl092021.pdf|Лекция 9. Операторы над типами: система λω]] 
21.04.2021 (ср) 13:45-15:45, online

[[Медиа:tapl102021.pdf|Лекция 10. Зависимые типы: система λP]] 
12.05.2021 (ср) 13:45-15:45, online

[[Медиа:tapl112021.pdf|Лекция 11. λ-куб и чистые системы типов]] 
19.05.2021 (ср) 13:45-15:45, online

[[Медиа:tapl122021.pdf|Лекция 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.

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

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

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

[https://docs.google.com/spreadsheets/d/1GzafZXasKQnV6sGblkpvRQVbXkXL6_iQQtp2oTB91rM/edit?usp=sharing гугл-табличка успеваемости]

Для образовательных программ с 5-бальной системой оценок проценты переводятся в баллы следующей функцией
 score :: Int -> Int
 score proc
   | proc < 51 = 0
   | proc > 98 = 5
   | otherwise = (proc - 51) `div` 8

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

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

Если вы ранее не обучались на Stepik, зарегистрироваться на [https://stepik.org/accounts/signup/ Stepik]. Настоятельная просьба - указать идентификационные данные, позволяющие опознавать вас без сложных исследований.

Перейти по [https://stepik.org/invitation/b6b56b90c41c55e8531e2d9b3c822c2e6fa16196/ ссылке-приглашению на курс]

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