HOL Light
HOL Light: an overview. HOL Light is an interactive proof assistant for classical higher-order logic, intended as a clean and simplified version of Mike Gordon’s original HOL system. Theorem provers in this family use a version of ML as both the implementation and interaction language; in HOL Light’s case this is Objective CAML (OCaml). Thanks to its adherence to the so-called `LCF approach’, the system can be extended with new inference rules without compromising soundness. While retaining this reliability and programmability from earlier HOL systems, HOL Light is distinguished by its clean and simple design and extremely small logical kernel. Despite this, it provides powerful proof tools and has been applied to some non-trivial tasks in the formalization of mathematics and industrial formal verification.
Keywords for this software
References in zbMATH (referenced in 308 articles )
Showing results 1 to 20 of 308.
Sorted by year (- Dubut, Jérémy; Yamada, Akihisa: Fixed points theorems for non-transitive relations (2022)
- Wieser, Eric; Song, Utensil: Formalizing geometric algebra in Lean (2022)
- Abbasi, Rosa; Schiffl, Jonas; Darulova, Eva; Ulbrich, Mattias; Ahrendt, Wolfgang: Deductive verification of floating-point Java programs in KeY (2021)
- Carette, Jacques; Farmer, William M.; Kohlhase, Michael; Rabe, Florian: Big math and the one-brain barrier: the tetrapod model of mathematical knowledge (2021)
- Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Machine learning guidance for connection tableaux (2021)
- Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef; Kumar, Ramana; Norrish, Michael: TacticToe: learning to prove with tactics (2021)
- Guan, Yong; Zhang, Jingzhi; Wang, Guohui; Li, Ximeng; Shi, Zhiping; Li, Yongdong: Formalization of Euler-Lagrange equation set based on variational calculus in HOL light (2021)
- Kohlhase, Michael; Rabe, Florian: Experiences from exporting major proof assistant libraries (2021)
- Mahboubi, Assia; Sibut-Pinote, Thomas: A formal proof of the irrationality of (\zeta(3)) (2021)
- Nipkow, Tobias; Roßkopf, Simon: Isabelle’s metalogic: formalization and proof checker (2021)
- Paulson, Lawrence C.: Ackermann’s function in iterative form: a proof assistant experiment (2021)
- Popescu, Andrei; Traytel, Dmitriy: Distilling the requirements of Gödel’s incompleteness theorems with a proof assistant (2021)
- Steen, Alexander; Benzmüller, Christoph: Extensional higher-order paramodulation in Leo-III (2021)
- Wang, Qingxiang; Kaliszyk, Cezary: JEFL: joint embedding of formal proof libraries (2021)
- Abrahamsson, Oskar: A verified proof checker for higher-order logic (2020)
- Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal: Scalable fine-grained proofs for formula processing (2020)
- Carneiro, Mario: Metamath Zero: designing a theorem prover prover (2020)
- Chen, Shanyan; Wang, Guohui; Li, Ximeng; Zhang, Qianying; Shi, Zhiping; Guan, Yong: Formalization of camera pose estimation algorithm based on Rodrigues formula (2020)
- Rashid, Adnan; Hasan, Osman: Formal verification of robotic cell injection systems up to 4-DOF using \textsfHOLLight (2020)
- Shi, Zhiping; Guan, Yong; Li, Ximeng: Formalization of complex analysis and matrix theory (2020)