Теорія математичних мов програмування

Робоча програма навчальної дисципліни (відповідно до вимог МОН України).
Документ містить мету, результати навчання, структуру змісту, систему оцінювання та літературу.

Код курсу: КА-121-06

Кафедра: Кафедра мовного забезпечення

Кількість кредитів ECTS: 6 (180 годин)

Рівень: Бакалавр / Магістр

Мета та завдання

Вивчення теорії мов програмування через ієрархію формальних систем Groupoid Infinity (репозиторії github.com/groupoid): від чистих типових систем до модальної гомотопічної теорії типів. Курс демонструє, як конструктивні засади (MLTT, CIC, HTS) реалізуються в мінімальних перевірячах типів і служать основою для формальної математики.

Результати навчання

• Пояснювати ієрархію систем: Henk → Frank → Christine → Per → Anders → Dan / Urs.
• Розрізняти PTS, CoC, CIC, MLTT-80 та модальну HoTT на рівні синтаксису, семантики та метатеорії.
• Розуміти роль індуктивних типів, ідентифікаційних типів, кубічних примітивів та модальностей.
• Аналізувати мінімальні реалізації перевірячів типів (розміри ядер, нормалізація, канонічність).
• Застосовувати формальні системи для простих доведень та формалізацій.

Структура курсу (модулі)

1. Вступ. Чисті типові системи та λ-куб. Henk (PTS / CoC∞)
   Лекційний матеріал: Pure Type Systems (Barendregt), Calculus of Constructions (Coquand–Huet), нескінченна ієрархія всесвітів, SAR-правила. Реалізація: Elixir/Erlang (~1400 LOC), OCaml-модель (~150 LOC), Miranda-подібний фронтенд, Böhm–Berarducci кодування. Репозиторій: github.com/groupoid/henk
2. Індуктивні конструкції. Frank (CoC + CIC)
   Лекційний матеріал: Calculus of Inductive Constructions, сувора позитивність, індуктивні типи поверх CoC. Мінімальне ядро з universe, Π та Inductive. Репозиторій: github.com/groupoid/frank
3. Загальна індукція та рівність. Christine (CIC + Fix / Id)
   Лекційний матеріал: розширення CIC загальною індукцією, фікспоінтами та ідентифікаційними типами. Тактичний прувер на Elixir з екстракцією в BEAM. Репозиторій: github.com/groupoid/christine
4. Інтуїціоністська теорія типів. Per (мінімальна MLTT-80 / CCHM)
   Лекційний матеріал: MLTT-80 (Martin-Löf), кубічні примітиви (Glue, Partial, Subtype, hcomp, transp), дві ієрархії всесвітів (U фібрант / V претипи). Самохостинг логіки. Репозиторій: github.com/groupoid/per
5. Модальна гомотопічна теорія типів. Anders (MLTT + HTS + кубічні примітиви + модальності)
   Лекційний матеріал: Modal HoTT, HTS (Voevodsky) зі строгою рівністю на претипах, CCHM/CHM, модальності (♭, ♯, ℑ — de Rham), Disc / Coequalizer / Hub-Spoke. Ядро ~2000 LOC, Lean-синтаксис. Репозиторій: github.com/groupoid/anders
6. Сімпліціальні розширення. Dan (∞-HoTT / GAP / simplicial)
   Лекційний матеріал: сімпліціальна теорія типів, Kan/Rezk/Segal режими, алгебраїчні конструкції (Chain, Category, Monoid, Group, Ring). Репозиторій: github.com/groupoid/dan
7. Когезивні модальності. Urs (♭, ♯, ℑ)
   Лекційний матеріал: когезивна гомотопічна теорія типів (Schreiber), flat/sharp/infinitesimal модальності поверх Anders. Репозиторій: github.com/groupoid/urs
8. Порівняння систем, екстракція, практична формалізація
   Порівняння розмірів ядер, метатеоретичних властивостей (нормалізація, канонічність, decidability), екстракція в BEAM/OCaml.
9. Практична лабораторна: робота з Anders / Per / Henk

Система оцінювання (100 балів)

• Поточний контроль (лабораторні, формалізації, рев’ю): 40 балів
• Модульні контрольні роботи (2): 20 балів
• Підсумковий іспит / захист проєкту (формалізація в одній із систем): 40 балів

Шкала: 90–100 — відмінно; 75–89 — добре; 60–74 — задовільно; <60 — незадовільно.

Рекомендована література

• Barendregt H. Lambda Calculi with Types. Handbook of Logic in Computer Science, 1992.
• Coquand T., Huet G. The Calculus of Constructions. Information and Computation, 1988.
• Martin-Löf P. Intuitionistic Type Theory. 1984.
• Voevodsky V. et al. Homotopy Type System (HTS).
• Cohen C., Coquand T., Huber S., Mörtberg A. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. 2016.
• Sokhatskyi M. Issue XI: Pure Type System (Henk); Issue XII: CIC (Frank); Issue XIX: Modal HTS (Anders). groupoid.space/books.
• Репозиторії: github.com/groupoid/{henk,frank,christine,per,anders,dan,urs}
• homotopy.dev — Anders Modal HTS.

← Назад до каталогу курсів