АссистентНовый вопросИсторияОбласти знаний
Партнёрские проектыСпецпроектыСтать автором
Сменить язык
О РУВИКИ

HOL

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) 2020-11-09. Дата обращения 2020-11-25. Используется устаревший параметр |deadlink= (справка)
  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) из оригинала 2020-11-30. Дата обращения 2020-11-25. Используется устаревший параметр |deadlink= (справка)
  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) 2020-09-19. Дата обращения 2020-11-25. Используется устаревший параметр |deadlink= (справка)

Категории