HOL
HOL (Higher Order Logic) — семейство инструментов интерактивного доказательства теорем, при создании которых были использованы схожие подходы к построению доказательств, основанные на логике высшего порядка и схожие подходы к реализации. HOL развивает подход системы LCF.
| HOL | |
|---|---|
| Автор | Майкл Гордон[англ.] |
| Расширение файлов |
.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] .
Литература
[править | править код]- Gordon, Michael J. C.. From LCF to HOL: A Short History (1996). Дата обращения: 11 октября 2007.
Ссылки
[править | править код]- Домашняя страница проекта HOL4
- Описание базовой логики HOL
- Руководство HOL4, включающее спецификацию логики работы системы.
- Virtual library formal methods information
Примечания
[править | править код]- ↑ CakeML. Дата обращения: 25 ноября 2020. Архивировано 14 сентября 2020 года.
- ↑ 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.
- ↑ 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.
- ↑ 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.