Например, Бобцов

ПРИМЕНЕНИЕ ЗАВИСИМЫХ СИСТЕМ ТИПОВ СО СТРУКТУРНОЙ ИНДУКЦИЕЙ ДЛЯ ВЕРИФИКАЦИИ РЕАКТИВНЫХ ПРОГРАММ

Аннотация:

Предлагается конструктивное доказательство (в виде программы на языке Agda) того, что решение задачи о выполнимости булевой формулы при помощи исчисления секвенций и верификация с использованием темпоральных спецификаций на языке CTL могут быть представлены в разрешимом подмножестве зависимой системы типов.

Читать текст статьи

Ключевые слова:

Статьи в номере