Теорія мов програмування

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

Код курсу: КВ-123-03

Кафедра: Кафедра теоретичної інформатики

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

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

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

Вивчення теорії мов програмування через мінімальні інтерпретатори категорних структур, системні академічні мови та класичні верифікатори. Курс охоплює внутрішні мови категорій (Alonzo, Yves), компілятори та віртуальні машини, а також підходи до формальної верифікації програмного забезпечення.

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

• Пояснювати внутрішні мови декартово-замкнених (Alonzo) та симетричних моноїдальних (Yves) категорій.
• Розуміти архітектуру мінімальних компіляторів і віртуальних машин (Tim, Max, Eijiro, Manfred).
• Аналізувати підходи до верифікації програм (Robin, Leslie, Andrea).
• Порівнювати різні моделі обчислень і їх реалізацію на рівні вихідного коду та семантики.
• Застосовувати теоретичні засади до аналізу та побудови інтерпретаторів.

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

1. Вступ. Внутрішні мови категорій. Alonzo — мінімальна внутрішня мова декартово-замкнених категорій
   Лекційний матеріал: просто типізоване λ-числення (Church), відповідність CCC ↔ STLC (Lambek), пари, проєкції, термінальний об’єкт. Реалізація: OCaml (STLC type checker). Репозиторій: github.com/groupoid/alonzo. Бібліографія: Church A. A Formulation of the Simple Theory of Types (1940); Guallart N. An Overview of Type Theories (2014).
2. Yves — мінімальна внутрішня мова симетричних моноїдальних категорій
   Лекційний матеріал: симетричні моноїдальні категорії, внутрішній гом, стрункові діаграми (Selinger, Joyal–Street). Мінімальна реалізація внутрішньої мови. Репозиторій: github.com/groupoid/yves.
3. Системні мови. Tim — компілятор і віртуальна машина Тіма Олсона (Miranda)
   Лекційний матеріал: лінива функціональна мова Miranda (Turner), комбінаторна редукція, SKI, патерн-матчинг. Архітектура мінімального компілятора та інтерпретатора.
4. Max — компілятор і віртуальна машина Максима Харченка (Erlang)
   Лекційний матеріал: Erlang/OTP, LING (Erlang on Xen), альтернативні віртуальні машини BEAM, динамічні інструкційні набори, обробка пам’яті без ОС.
5. Eijiro — компілятор і віртуальна машина Ейджиро Сумії (Caml / MinCaml)
   Лекційний матеріал: MinCaml — мінімальний компілятор ML-підмножини (~2000 рядків OCaml) до SPARC assembly, освітній компілятор функціональних мов. Роботи Sumii з бісимуляцій, типової абстракції, Fail-Safe C.
6. Manfred — системна академічна мова програмування Манфреда Броя
   Лекційний матеріал: алгебраїчна семантика мов програмування, трансформаційна розробка програм, аплікативні мови, специфікація через абстрактні типи даних (Broy, Wirsing, Pepper).
7. Верифікатори. Robin — перший верифікатор ПЗ Робіна Мілнера
   Лекційний матеріал: LCF (Logic for Computable Functions), ML як метамова, тактики, премія Тюрінга за ML та поліморфну типову систему.
8. Leslie — верифікатор розподілених протоколів TLA+ Леслі Лампорта
   Лекційний матеріал: Temporal Logic of Actions, TLA+, специфікація та перевірка розподілених систем у просторі та часі.
9. Andrea — сертифікована тактична система доведення теорем з ядром Coq Андреа Асперті
   Лекційний матеріал: тактичні системи поверх ядра Coq, сертифіковані прувери, роботи Asperti з формальної математики та тактик.
10. Практична лабораторна: аналіз або мінімальна реалізація одного з інтерпретаторів

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

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

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

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

• Church A. A Formulation of the Simple Theory of Types. 1940.
• Lambek J., Scott P.J. Introduction to Higher Order Categorical Logic. 1986.
• Selinger P. A Survey of Graphical Languages for Monoidal Categories. 2011.
• Turner D.A. Miranda: A Non-Strict Functional Language with Polymorphic Types. 1985.
• Sumii E. MinCaml: a simple and efficient compiler for a minimal functional language. 2005.
• Broy M., Wirsing M., Pepper P. On the Algebraic Definition of Programming Languages. 1986.
• Milner R. LCF: A Logic for Computable Functions.
• Lamport L. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. 2002.
• Репозиторії: github.com/groupoid/{alonzo,yves} та матеріали Groupoid Infinity.
• Класичні підручники з семантики мов програмування та формальної верифікації.

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