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] .
Литература
- 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 года.
- ↑ Verified LISP Implementations on ARM, x86 and PowerPC // (TPHOLs 2009). — P. 359–374.
- ↑ (2010) «x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors». Communications of the ACM 53 (7): 89–97. doi:10.1145/1785414.1785443.
- ↑ The Semantics of Power and ARM Multiprocessor Machine Code // (DAMP 2009). — P. 13–24.