Interested Article - HOL

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

Логика реализации

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

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

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

Литература

(неопр.) (1996). Дата обращения: 11 октября 2007.

Ссылки

.

Примечания

(неопр.) . Дата обращения: 25 ноября 2020. 14 сентября 2020 года.
Magnus O. Myreen; Michael J. C. Gordon. (PDF) . TPHOLs 2009. pp. 359—374. Архивировано из (PDF) 9 ноября 2020 . Дата обращения: 25 ноября 2020 .
Peter Sewell; Susmit Sarkar; Scott Owens; Francesco Zappa Nardelli; Magnus O. Myreen (2010). (PDF) . Communications of the ACM . 53 (7): 89—97. doi : . (PDF) из оригинала 30 ноября 2020 . Дата обращения: 25 ноября 2020 .
Jade Alglave; Anthony C. J. Fox; Samin Ishtiaq; Magnus O. Myreen; Susmit Sarkar; Peter Sewell; Francesco Zappa Nardelli. (PDF) . DAMP 2009. pp. 13—24. Архивировано из (PDF) 19 сентября 2020 . Дата обращения: 25 ноября 2020 .