УДК: 004.423

Формальная модель вычислений с плавающей точкой на основе лямбда-исчисления с зависимыми типами

С. В. Антонов, студент, e-mail: antonovsergey93@gmail.com, М. А. Кривчиков, науч. сотр., e-mail: maxim.krivchikov@gmail.com, Механико-математический факультет и НИИ механики МГУ имени М. В. Ломоносова, г. Москва

Одним из важных аспектов формальной верификации программных комплексов моделирования физических процессов является доказательство корректности реализации используемых вычислительных методов. Для вычислений в высокопроизводительных средах моделирования, как правило, используют числа с плавающей точкой, соответствующие стандарту IEEE 754. В настоящей статье представлены результаты работы по построению формальной модели чисел с плавающей точкой на основе положений стандарта IEEE 754 в среде Coq и адаптированная версия этой модели для широкого класса реализаций лямбда-исчисления с зависимыми типами. Модель является исполнимой, что позволяет в том числе получать с ее помощью результаты вычислений в среде Coq.

Ключевые слова: формальные модели, формальная верификация, лямбда-исчисление, программирование с зависимыми типами, числа с плавающей точкой, погрешность вычислений, формальная семантика

Стр. 25–31