HOL

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

HOL
Автор en:Michael J C Gordon
Расширение файлов .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] .

Литература

Ссылки

Примечания
  1. CakeML.
  2. «Verified LISP Implementations on ARM, x86 and PowerPC» in TPHOLs 2009.: 359–374.
  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.
  4. «The Semantics of Power and ARM Multiprocessor Machine Code» in DAMP 2009.: 13–24.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.