HOL

HOL (Higher Order Logic) — семейство инструментов интерактивного доказательства теорем, при создании которых были использованы схожие подходы к построению доказательств, основанные на логике высшего порядка и схожие подходы к реализации. HOL развивает подход системы LCF.

HOL
Автор	Майкл Гордон[англ.]
Расширение файлов	.sml
Лицензия	Modified (3-clause) BSD licence
Сайт	hol-theorem-prover.org

Избранные проекты, использовавшие HOL

С использованием были разработаны доказательства формальной корректности в проекте CakeML^[1] — формально специфицированной и верифицированной версии языка ML. До этого HOL использовался для реализации формально специфицированной и верифицированной версии LISP, работавшей на процессорах ARM, x86 и PowerPC^[2].

HOL так же использовался для разработки формальной семантики для варианта мултипроцессорных систем x86^[3], а также для определения формальной семантики наборов инструкций Power ISA и ARM^[4] .

Литература

• Gordon, Michael J. C.. From LCF to HOL: A Short History  (неопр.) (1996). Дата обращения: 11 октября 2007.

Ссылки

• Домашняя страница проекта HOL4
• Описание базовой логики HOL
• Руководство HOL4, включающее спецификацию логики работы системы.
• Virtual library formal methods information