Editing HOL (proof assistant) (section)

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

# HOL4 {{emdash}} 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 (computer scientist)|Mike Gordon]]. HOL88 included its own [[ML (programming language)|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 [[Coupling (computer programming)|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.<ref>{{Cite web | url=http://hol-theorem-prover.org/ | title=HOL Interactive Theorem Prover}}</ref>
# [[HOL Light]] {{emdash}} 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.<ref>{{Cite web | url=http://www.cl.cam.ac.uk/users/jrh/hol-light/ |title = HOL Light}}</ref>
# [http://www.lemma-one.com/ProofPower/index/ ProofPower] {{emdash}} a collection of six tools designed to provide special support grounded in HOL for working with the [[Z notation]] for formal specification. The tool PPDaz supporting specification and verification of programs written in a subset of Ada was previously only supplied under a proprietary licence. All the tools are now available under the GNU GPL v2 license.
# [http://proof-technologies.com/holzero/index.html HOL Zero] {{emdash}} a minimalist implementation focused on trustworthiness. HOL Zero is GNU GPL 3+ licensed.<ref>See LICENSE file in the [http://proof-technologies.com/holzero-0.5.3.tgz tarball] {{Webarchive|url=https://web.archive.org/web/20120303154208/http://proof-technologies.com/holzero-0.5.3.tgz |date=2012-03-03 }}.</ref>
# [https://cakeml.org/candle.html Candle] {{emdash}}  An end-to-end verified HOL Light implementation on top of CakeML.<ref>{{Cite journal |last1=Abrahamsson |first1=Oskar |last2=Myreen |first2=Magnus O. |last3=Kumar |first3=Ramana |last4=Sewell |first4=Thomas |date=2022 |editor-last=Andronick |editor-first=June |editor2-last=de Moura |editor2-first=Leonardo |title=Candle: A Verified Implementation of HOL Light |url=https://drops.dagstuhl.de/opus/volltexte/2022/16712 |journal=13th International Conference on Interactive Theorem Proving (ITP 2022) |series=Leibniz International Proceedings in Informatics (LIPIcs) |location=Dagstuhl, Germany |publisher=Schloss Dagstuhl – Leibniz-Zentrum für Informatik |volume=237 |pages=3:1–3:17 |doi=10.4230/LIPIcs.ITP.2022.3 |doi-access=free |isbn=978-3-95977-252-5|s2cid=251323103 }}</ref>