Освітня програма «Формальні мови програмування»
Кафедра мовного забезпечення
Рівень вищої освіти: другий (магістерський)
Спеціальність: 121 Інженерія програмного забезпечення
Галузь знань: 12 Інформаційні технології
1. Мета освітньої програми
Підготовка фахівців, здатних здійснювати дослідження, розробку та формальну верифікацію мов програмування, компіляторів, інтерпретаторів і системного програмного забезпечення. Програма поєднує класичну теорію компіляторів, історію мов програмування, сучасні формальні системи та механічну верифікацію.
2. Програмні результати навчання
- Проєктувати та реалізовувати генератори компіляторів і інтерпретаторів (LL/LR/LALR, PEG, рекурсивний спуск).
- Аналізувати мови програмування за таксономією формальних характеристик.
- Застосовувати методи формальної верифікації (Coq/Rocq, нуль аксіом).
- Розуміти ієрархію сучасних формальних систем (PTS, CIC, HoTT).
- Оцінювати історичний та теоретичний контекст мов програмування.
3. Навчальний план (магістерський рівень, 90 кредитів ECTS, 1,5 роки)
| Семестр | Дисципліна | Код | Кредити | Контроль |
|---|---|---|---|---|
| 1 | Генератор компіляторів | КА-121-01 | 12 | Іспит |
| Теорія математичних мов програмування | КА-121-06 | 6 | Іспит | |
| Історія мов програмування | КА-121-07 | 6 | Залік | |
| 2 | Верифікація ПЗ | КА-121-04 | 6 | Іспит |
| Верифікація мікропроцесорів | КА-121-03 | 6 | Іспит | |
| Верифікація об’єктного коду | КА-121-05 | 6 | Залік | |
| 3 | Інтерпретатори | КА-121-02 | 6 | Іспит |
| Курсова робота | — | 3 | Залік | |
| Науково-дослідна практика | — | 7 | Залік | |
| Кваліфікаційна (дипломна) робота | — | 32 | Захист | |
| Разом | 90 | |||
4. Робочі програми дисциплін
Детальні робочі програми інтегровані в сторінки курсів кафедри мовного забезпечення.