Editing HOL (proof assistant)

{{Short description|Interactive theorem proving systems}}
{{Infobox programming language
| name = HOL
| designer = [[Michael J C Gordon]]
| license = [[BSD licenses|Modified (3-clause) BSD license]]
| website = {{url|hol-theorem-prover.org}}
| file_ext = .sml
}}

'''HOL''' ('''Higher Order Logic''') denotes a family of [[Proof assistant|interactive theorem proving systems]] using similar [[Higher-order logic|(higher-order)]] logics and implementation strategies. Systems in this family follow the [[LCF (theorem prover)|LCF]] (Logic for Computable Functions) approach as they are implemented as a library which defines an [[abstract data type]] of proven [[theorem]]s such that new objects of this type can only be created using the functions in the library which correspond to [[inference rule]]s 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 (programming language)|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==
{{expand section|date=October 2021}}

HOL systems use variants of [[classical logic|classical]] [[higher-order logic]], which has simple axiomatic foundations with few axioms and well-understood semantics.<ref>{{cite book|last=Andrews|first=Peter B|year=2002|title=An introduction to mathematical logic and type theory: to truth through proof|edition=Second|series=Applied Logic Series|volume=27|isbn=978-1-4020-0763-7|publisher=Kluwer Academic Publishers|location=Dordrecht}}</ref>

The logic used in HOL provers is closely related to Isabelle/HOL,<ref>{{cite book|author1=Tobias Nipkow|author2=Markus Wenzel|author3-link=Lawrence C. Paulson|author3=Lawrence C. Paulson|year=2002|title=Isabelle/HOL: A Proof Assistant for Higher-Order Logic|publisher=Springer-Verlag|location=Berlin, Heidelberg|isbn=978-3-540-45949-1|author1-link=Tobias Nipkow}}</ref> the most widely used logic of [[Isabelle (proof assistant)|Isabelle]].

==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>

==Formal proof developments==
{{expand section|date=October 2021}}

The [[Standard ML#Implementations|CakeML]] project developed a formally proven compiler for ML.<ref>{{Cite web | url=https://cakeml.org/ |title = CakeML}}</ref> Previously, HOL was used to develop a formally proven [[Lisp (programming language)|Lisp]] implementation running on ARM, x86 and PowerPC.<ref>{{cite conference|author1=Magnus O. Myreen|author2=Michael J. C. Gordon|title=Verified LISP Implementations on ARM, x86 and PowerPC|conference=TPHOLs 2009|pages=359–374|url=https://www.cl.cam.ac.uk/~mom22/tphols09-lisp.pdf}}</ref>

HOL was also used to formalize the [[semantics (computer science)|semantics]] of x86 multiprocessors<ref>{{cite journal|author1=Peter Sewell|author2=Susmit Sarkar|author3=Scott Owens|author4=Francesco Zappa Nardelli|author5=Magnus O. Myreen|title=x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors|journal=[[Communications of the ACM]]|volume=53|issue=7|pages=89–97|year=2010|url=https://www.cl.cam.ac.uk/~pes20/weakmemory/cacm.pdf|doi=10.1145/1785414.1785443|s2cid=1999974}}</ref> as well as the [[machine code]] for [[Power ISA]] and [[ARM architecture|ARM]] architectures.<ref>{{cite conference|author1=Jade Alglave|author1-link=Jade Alglave|author2=Anthony C. J. Fox|author3=Samin Ishtiaq|author4=Magnus O. Myreen|author5=Susmit Sarkar|author6=Peter Sewell|author7=Francesco Zappa Nardelli|title=The Semantics of Power and ARM Multiprocessor Machine Code|conference=DAMP 2009|pages=13–24|url=http://www0.cs.ucl.ac.uk/staff/j.alglave/papers/damp09.pdf}}</ref>

==References==
{{reflist}}

==Further reading==
* {{cite web
  | last = Gordon
  | first = Michael J. C.
  | author-link = Michael J. C. Gordon
  | year = 1996
  | title = From LCF to HOL: A Short History
  | url = http://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.html
  | access-date = 2007-10-11 }}

==External links==
* {{Official website|hol-theorem-prover.org}}
* [http://www.lemma-one.com/ProofPower/specs/specs.html Documents specifying HOL's basic logic]
* [http://prdownloads.sourceforge.net/hol/kananaskis-3-description.pdf?download HOL4 Description manual], includes system logic specification
* [https://web.archive.org/web/20051219153731/http://vl.fmnet.info/hol/ Virtual library formal methods information]

{{ML programming}}

[[Category:Proof assistants]]
[[Category:Logic in computer science]]
[[Category:Software using the BSD license]]