В этом году курс посвящён в основном типизованным вариантам λ-исчисления, в т.ч. системам более высоких порядков, таким как система F, а также возможностям таковых систем по представлению доказуемо тотальных вычислимых функций.

Литература:

• M. Sørensen, P. Urzyczyn. Lectures on the Curry-Howard isomorphism.
• J.-Y. Girard. Proofs and types, translated and with appendices by P. Taylor and Y. Lafont.

Расписание на осенний семестр 2022/2023 учебного года:

Время занятий: вторник 16:25 – 17:50

Первое занятие: 13 сентября. Занятия закончились 29 ноября.

Задачи: часть 1 (№№ 1–7); часть 2 (№№ 8–14); часть 3 (№№ 15–20)

К экзамену: основные теоретические вопросы

Финансовая поддержка. Курс проводится при финансовой поддержке Минобрнауки России (грант на создание и развитие МЦМУ МИАН, соглашение № 075-15-2022-265).

Лектор
Кузнецов Степан Львович

Организации
Московский физико-технический институт (государственный университет), г. Долгопрудный, Московская обл.
Математический институт им. В.А. Стеклова Российской академии наук, г. Москва
Математический центр мирового уровня «Математический институт им. В.А. Стеклова Российской академии наук» (МЦМУ МИАН)