Types 25

Типы в языках программирования

Осенний курс по выбору для студентов 3 и 4 курсов ПМИ ФКН ВШЭ.

Лектор: Павел Соколов aka @TurtlePU.

Семинарист: Илья Григорьев aka @ilyagribun.

Ассистент: Ислам Талипов aka @lishy2.

Полезные ссылки

Канал курса (Telegram)

Чат курса (Telegram)

Лекции (Zoom)

[TBA Семинары (Zoom)]

[TBA Записи занятий (Я.Диск)]

[TBA classroom для сдачи теоретических домашних заданий]

[TBA classroom для сдачи практических домашних заданий]

[TBA Оценки]

Программа учебной дисциплины

Лекции и семинары

• Лекция 1, 16 сен 2025. Организация курса; Формальные методы и теория типов; Язык NatBool, его денотационная семантика и здравость системы типов относительно неё. [TBA Запись].
• Семинар 1, 19 сен 2025. TBA. [TBA Запись].
• Лекция 2, 23 сен 2025. TBA. [TBA Запись].
• Семинар 2, 23 сен 2025. TBA. [TBA Запись].

Домашние задания

• ТДЗ-1 (теоретическое). TBA. [TBA Условие]. [TBA Исходник]. Дедлайн: TBA.

Условие теоретических домашних заданий скомпилировано с помощью pdfLaTeX.

Итоговая оценка за курс

Итог = Округление(0.4 * ТДЗ + 0.4 * ПДЗ + 0.2 * Э + Б),

где ТДЗ – средняя оценка за теоретические домашние задания, ПДЗ – за практические, Э - оценка за экзамен, а Б – сумма бонусных баллов, полученных за курс.

Округление арифметическое.

Автоматы за экзамен TBA.

Литература

Основная литература

1. Benjamin C. Pierce, Types and Programming Languages
2. Frank Pfenning, Lecture Notes on Bidirectional Type Checking
3. Jean-Yves Girard, Proofs and Types
4. Arend Theorem Prover

Дополнительная литература

1. Lectures on the Curry-Howard Isomorphism
2. The Twelf Project
3. Programming Language and Theorem Prover – Lean
4. The Granule Project