HOL

HOL
Автор en:Michael J C Gordon
Расширение файлов .sml
Лицензия Modified (3-clause) BSD licence
Сайт hol-theorem-prover.org

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

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

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

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

Литература

Ссылки

Примечания

  1. ↑ CakeML. Дата обращения: 25 ноября 2020. Архивировано 14 сентября 2020 года.
  2. ↑ Magnus O. Myreen; Michael J. C. Gordon. Verified LISP Implementations on ARM, x86 and PowerPC (PDF). TPHOLs 2009. pp. 359—374. Архивировано из оригинала (PDF) 9 ноября 2020. Дата обращения: 25 ноября 2020.
  3. ↑ Peter Sewell; Susmit Sarkar; Scott Owens; Francesco Zappa Nardelli; Magnus O. Myreen (2010). "x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors" (PDF). Communications of the ACM. 53 (7): 89—97. doi:10.1145/1785414.1785443. Архивировано (PDF) 30 ноября 2020. Дата обращения: 25 ноября 2020.
  4. ↑ Jade Alglave; Anthony C. J. Fox; Samin Ishtiaq; Magnus O. Myreen; Susmit Sarkar; Peter Sewell; Francesco Zappa Nardelli. The Semantics of Power and ARM Multiprocessor Machine Code (PDF). DAMP 2009. pp. 13—24. Архивировано из оригинала (PDF) 19 сентября 2020. Дата обращения: 25 ноября 2020.