HOL (proof assistant)
| Designed by | Michael J C Gordon |
|---|---|
| License | Modified (3-clause) BSD licence |
| Filename extensions | .sml |
| Website | hol-theorem-prover |
HOL (Higher Order Logic) denotes a family of interactive theorem proving systems using similar (higher-order) logics and implementation strategies. Systems in this family follow the LCF approach as they are implemented as a library which defines an abstract data type of proven theorems such that new objects of this type can only be created using the functions in the library which correspond to 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:
- 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 Mike Gordon. HOL88 included its own ML implementation, which was in turn implemented on top of Common Lisp. The systems that followed HOL88 (HOL90, hol98 and HOL4) were all implemented in Standard ML; while hol98 is coupled to Moscow ML, HOL4 can be built with either Moscow ML or 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]
- HOL Light — an experimental "minimalist" version of HOL which has since grown into another mainstream HOL variant; its logical foundations remain unusually simple. HOL Light, originally implemented in Caml Light, now uses OCaml. HOL Light is available under the new BSD license.[4]
- 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]
- HOL Zero — a minimalist implementation focused on trustworthiness. HOL Zero is GNU GPL 3+ licensed.[6]
- 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 semantics of x86 multiprocessors[10] as well as the machine code for Power ISA and ARM architectures.[11]
References
- ↑ Andrews, Peter B (2002). An introduction to mathematical logic and type theory: to truth through proof. Applied Logic Series. 27 (Second ed.). Dordrecht: Kluwer Academic Publishers. ISBN 978-1-4020-0763-7.
- ↑ Tobias Nipkow; Markus Wenzel; Lawrence C. Paulson (2002). Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Berlin, Heidelberg: Springer-Verlag. ISBN 978-3-540-45949-1.
- ↑ "HOL Interactive Theorem Prover". http://hol-theorem-prover.org/.
- ↑ "HOL Light". http://www.cl.cam.ac.uk/users/jrh/hol-light/.
- ↑ "Getting ProofPower". http://www.lemma-one.com/ProofPower/getting/.
- ↑ See LICENSE file in the tarball .
- ↑ Abrahamsson, Oskar; Myreen, Magnus O.; Kumar, Ramana; Sewell, Thomas (2022). Andronick, June; de Moura, Leonardo. eds. "Candle: A Verified Implementation of HOL Light". 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs) (Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum für Informatik) 237: 3:1–3:17. doi:10.4230/LIPIcs.ITP.2022.3. ISBN 978-3-95977-252-5. https://drops.dagstuhl.de/opus/volltexte/2022/16712.
- ↑ "CakeML". https://cakeml.org/.
- ↑ Magnus O. Myreen; Michael J. C. Gordon. "Verified LISP Implementations on ARM, x86 and PowerPC". TPHOLs 2009. pp. 359–374. https://www.cl.cam.ac.uk/~mom22/tphols09-lisp.pdf.
- ↑ 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". Communications of the ACM 53 (7): 89–97. doi:10.1145/1785414.1785443. https://www.cl.cam.ac.uk/~pes20/weakmemory/cacm.pdf.
- ↑ 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". DAMP 2009. pp. 13–24. http://www0.cs.ucl.ac.uk/staff/j.alglave/papers/damp09.pdf.
Further reading
- Gordon, Michael J. C. (1996). "From LCF to HOL: A Short History". http://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.html.
External links
- HOL4 Project homepage
- Documents specifying HOL's basic logic
- The HOL4 Description manual, which includes a specification of the system's logic.
- Virtual library formal methods information
 |  |
