HOL (Higher Order Logic) — семейство инструментов интерактивного доказательства теорем, при создании которых были использованы схожие подходы к построению доказательств, основанные на логике высшего порядка и схожие подходы к реализации. HOL развивает подход системы LCF.
Избранные проекты, использовавшие HOL С использованием были разработаны доказательства формальной корректности в проекте CakeML — формально специфицированной и верифицированной версии языка ML. До этого HOL использовался для реализации формально специфицированной и верифицированной версии LISP, работавшей на процессорах ARM, x86 и PowerPC.
HOL так же использовался для разработки формальной семантики для варианта мултипроцессорных систем x86, а также для определения формальной семантики наборов инструкций Power ISA и ARM .
Литература
Ссылки Домашняя страница проекта HOL4 Описание базовой логики HOL Руководство HOL4, включающее спецификацию логики работы системы. Virtual library formal methods information
Примечания
Категория:Функциональное программирование Категория:Инструменты интерактивного доказательства теорем Категория:Программное обеспечение, написанное на ML