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 284 articles )
Showing results 1 to 20 of 284.
Sorted by year (- 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)
- Beeson, Michael; Narboux, Julien; Wiedijk, Freek: Proof-checking Euclid (2019)
- Beillahi, Sidi Mohamed; Mahmoud, Mohamed Yousri; Tahar, Sofiène: A modeling and verification framework for optical quantum circuits (2019)
- Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef: GRUNGE: a grand unified ATP challenge (2019)
- Carette, Jacques; Farmer, William M.: Towards specifying symbolic computation (2019)
- Gauthier, Thibault; Kaliszyk, Cezary: Aligning concepts across proof assistant libraries (2019)
- Kunčar, Ondřej; Popescu, Andrei: From types to sets by local type definition in higher-order logic (2019)
- Kunčar, Ondřej; Popescu, Andrei: A consistent foundation for Isabelle/HOL (2019)
- Li, Li-Ming; Shi, Zhi-Ping; Guan, Yong; Zhang, Qian-Ying; Li, Yong-Dong: Formalization of geometric algebra in HOL Light (2019)
- Magron, Victor; Safey El Din, Mohab; Schweighofer, Markus: Algorithms for weighted sum of squares decomposition of non-negative univariate polynomials (2019)
- Marić, Filip: Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points (2019)
- Miller, Dale: Mechanized metatheory Revisited (2019)
- Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio: The Coq library as a theory graph (2019)
- Narboux, Julien; Janičić, Predrag; Fleuriot, Jacques: Computer-assisted theorem proving in synthetic geometry (2019)
- Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
- Raggi, Daniel; Stockdill, Aaron; Jamnik, Mateja; Garcia Garcia, Grecia; Sutherland, Holly E. A.; Cheng, Peter C.-H.: Inspection and selection of representations (2019)
- Rashid, Adnan; Hasan, Osman: Formal analysis of continuous-time systems using Fourier transform (2019)
- Stojanović-Ðurđević, Sana: From informal to formal proofs in Euclidean geometry (2019)
- Zhang, Jingzhi; Wang, Guohui; Shi, Zhiping; Guan, Yong; Li, Yongdong: Formalization of functional variation in HOL Light (2019)