Верифікація перетворення між винятково функційною та імперативною предметно-орієнтованими мовами програмування на прикладі HELIX

HELIX є формально верифікованим ланцюжком мов програмування та правил перекладу, призначеним для генерації високоефективних імплементацій ряду чисельних алгоритмів. Будучи заснованим на існуючій системі SPIRAL, HELIX додає строгість формального доведення коректності з використанням інструменту інтерактивного доведення теорем Coq. Він формально описує набір предметно-орієнтованих мов, починаючи з HCOL, що задає абстрактний потік даних обчислення. Робота HELIX полягає в перетворенні початкової програми через низку проміжкових мов, що закінчується на LLVM IR.
В даній роботі описані три мови цього ланцюжка та формальна верифікація переходу між ними. Розглянуті переходи є нетривіальним, адже кожна наступна мова ланцюжка вводить абстракції нижчого рівня, у порівнянні з попередньою. Відбувається перехід від чисто функційної мови змішаного рівня вбудови до глибоко вбудованої імперативної, від абстрактного алгебраїчного типу даних до машинних чисел з рухомою комою, додається модель пам’яті, області видимості змінних та монадна обробка винятків. Продемонстрована архітектура цих мов, автоматичний перехід між ними та автоматизоване доведення збереження семантики на кожному з кроків.

Зайчук І. К. Верифікація перетворення між винятково функційною та імперативною предметно-орієнтованими мовами програмування на прикладі HELIX : дипломна робота ... бакалавра : 122 Комп’ютерні науки / Зайчук Ілля Костянтинович. - Київ, 2021. - 40 с.