HOL (proof assistant)

Source: Wikipedia, the free encyclopedia.
HOL
Michael J C Gordon
LicenseModified (3-clause) BSD licence
Filename extensions.sml
Websitehol-theorem-prover.org

HOL (Higher Order Logic) denotes a family of

inference rules in higher-order logic
. As long as these functions are correctly implemented, all theorems proven in the system must be valid. As such, a large system can be built on top of a small trusted kernel.

Systems in the HOL family use ML or its successors. ML was originally developed along with LCF as a meta-language for theorem proving systems; in fact, the name stands for "Meta-Language".

Underlying logic

HOL systems use variants of classical higher-order logic, which has simple axiomatic foundations with few axioms and well-understood semantics.[1]

The logic used in HOL provers is closely related to Isabelle/HOL,[2] the most widely used logic of Isabelle.

HOL implementations

A number of HOL systems (sharing essentially the same logic) remain active and in use:

  1. HOL4 — the only presently maintained and developed system stemming from the HOL88 system, which was the culmination of the original HOL implementation effort, led by
    Poly/ML. All come with large libraries of theorem proving code which implement extra automation on top of the very simple core code. HOL4 is BSD licensed.[3]
  2. Caml Light, now uses OCaml. HOL Light is available under the new BSD license.[4]
  3. ProofPower — a collection of tools designed to provide special support for working with the Z notation for formal specification. 5 of the 6 tools are GNU GPL v2 licensed. The sixth (PPDaz) has a proprietary license.[5]
  4. HOL Zero — a minimalist implementation focused on trustworthiness. HOL Zero is GNU GPL 3+ licensed.[6]
  5. Candle — An end-to-end verified HOL Light implementation on top of CakeML.[7]

Formal proof developments

The CakeML project developed a formally proven compiler for ML.[8] Previously, HOL was used to develop a formally proven Lisp implementation running on ARM, x86 and PowerPC.[9]

HOL was also used to formalize the

ARM architectures.[11]

References

  1. ISBN 978-1-4020-0763-7
    .
  2. ISBN 978-3-540-45949-1
    .
  3. ^ "HOL Interactive Theorem Prover".
  4. ^ "HOL Light".
  5. ^ "Getting ProofPower".
  6. ^ See LICENSE file in the tarball Archived 2012-03-03 at the Wayback Machine.
  7. S2CID 251323103
    .
  8. ^ "CakeML".
  9. ^ Magnus O. Myreen; Michael J. C. Gordon. Verified LISP Implementations on ARM, x86 and PowerPC (PDF). TPHOLs 2009. pp. 359–374.
  10. S2CID 1999974
    .
  11. ^ 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.

Further reading

External links

Retrieved from "https://en.wikipedia.org/w/index.php?title=HOL_(proof_assistant)&oldid=1211076262"