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 189 articles )
Showing results 1 to 20 of 189.
Sorted by year (- 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)
- Cheung, Kevin K.H.; Gleixner, Ambros; Steffy, Daniel E.: Verifying integer programming results (2017)
- Coghetto, Roland: Pascal’s theorem in real projective plane (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)
- 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)
- Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian: Classification of alignments between concepts of formal mathematical systems (2017)
- Papapanagiotou, Petros; Fleuriot, Jacques: WorkflowFM: a logic-based framework for formal process specification and composition (2017)
- Rashid, Adnan; Hasan, Osman: Formalization of transform methods using HOL Light (2017)
- Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp: An approximation framework for solvers and decision procedures (2017)
- Adams, Mark: HOL zero’s solutions for Pollack-inconsistency (2016)
- Arthan, Rob: On definitions of constants and types in HOL (2016)
- Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody: A heuristic prover for real inequalities (2016)
- Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
- Boldo, Sylvie; Lelay, Catherine; Melquiond, Guillaume: Formalization of real analysis: a survey of proof assistants and libraries (2016)
- Chatzikyriakidis, Stergios; Luo, Zhaohui: Proof assistants for natural language semantics (2016)
- Kevin K. H. Cheung, Ambros Gleixner, Daniel E. Steffy: Verifying Integer Programming Results (2016) arXiv
- Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott: Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation (2016)
- Ma, Sha; Shi, Zhiping; Li, Liming; Guan, Yong; Zhang, Jie; Song, Xiaoyu: Formalization of geometric algebra theories in higher-order logic (2016)
- Ma, Sha; Shi, Zhiping; Shao, Zhenzhou; Guan, Yong; Li, Liming; Li, Yongdong: Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm (2016)