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 227 articles )
Showing results 1 to 20 of 227.
Sorted by year (- Gauthier, Thibault; Kaliszyk, Cezary: Aligning concepts across proof assistant libraries (2019)
- Rashid, Adnan; Hasan, Osman: Formal analysis of continuous-time systems using Fourier transform (2019)
- Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
- Farmer, William M.: Incorporating quotation and evaluation into Church’s type theory (2018)
- Maggesi, Marco: A formalization of metric spaces in HOL light (2018)
- Allamigeon, Xavier; Katz, Ricardo D.: A formalization of convex polyhedra based on the simplex method (2017)
- Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy: Friends with benefits. Implementing corecursion in foundational proof assistants (2017)
- Carter, Nathan C.; Monks, Kenneth G.: A web-based toolkit for mathematical word processing applications with semantics (2017)
- Cauderlier, Raphaël; Dubois, Catherine: Focalize and dedukti to the rescue for proof interoperability (2017)
- Cheung, Kevin K. H.; Gleixner, Ambros; Steffy, Daniel E.: Verifying integer programming results (2017)
- Chiang, Wei-Fan; Baranowski, Mark; Briggs, Ian; Solovyev, Alexey; Gopalakrishnan, Ganesh; Rakamarić, Zvonimir: Rigorous floating-point mixed-precision tuning (2017)
- Coghetto, Roland: Pascal’s theorem in real projective plane (2017)
- Cruz-Filipe, Luís; Larsen, Kim S.; Schneider-Kamp, Peter: Formally proving size optimality of sorting networks (2017)
- Farmer, William M.: Theory morphisms in Church’s type theory with quotation and evaluation (2017)
- Ford, Ian: Semantic representation of general topology in the Wolfram language (2017)
- Gabrielli, Andrea; Maggesi, Marco: Formalizing basic quaternionic analysis (2017)
- Geuvers, Herman (ed.); England, Matthew (ed.); Hasan, Osman (ed.); Rabe, Florian (ed.); Teschke, Olaf (ed.): Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17--21, 2017. Proceedings (2017)
- Gilbert, Frédéric: Proof certificates in PVS (2017)
- Hales, Thomas; Adams, Mark; Bauer, Gertrud; Dang, Tat Dat; Harrison, John; Hoang, Le Truong; Kaliszyk, Cezary; Magron, Victor; McLaughlin, Sean; Nguyen, Tat Thang; Nguyen, Quang Truong; Nipkow, Tobias; Obua, Steven; Pleso, Joseph; Rute, Jason; Solovyev, Alexey; Ta, Thi Hoai An; Tran, Nam Trung; Trieu, Thi Diep; Urban, Josef; Vu, Ky; Zumkeller, Roland: A formal proof of the Kepler conjecture (2017)
- Kohlhase, Michael; Müller, Dennis; Owre, Sam; Rabe, Florian: Making PVS accessible to generic services by interpretation in a universal format (2017)