×

HOL Light

swMATH ID: 6580
Software Authors: Harrison, John
Description: 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.
Homepage: http://www.cl.cam.ac.uk/~jrh13/hol-light/
Programming Languages: Objective CAML (OCaml)
Related Software: Coq; Isabelle/HOL; HOL; Isabelle; Mizar; ML; PVS; Flyspeck; z3; ACL2; E Theorem Prover; Sledgehammer; TPTP; Agda; VAMPIRE; kepler98; Archive Formal Proofs; Metis_; Nuprl; Isar
Cited in: 320 Documents
all top 5

Cited by 389 Authors

36 Kaliszyk, Cezary
23 Urban, Josef
17 Tahar, Sofiène
15 Rabe, Florian
13 Paulson, Lawrence Charles
12 Blanchette, Jasmin Christian
10 Hasan, Osman
10 Popescu, Andrei
9 Guan, Yong
8 Kumar, Ramana
8 Myreen, Magnus O.
8 Shi, Zhiping
7 Benzmüller, Christoph Ewald
7 Farmer, William M.
7 Gauthier, Thibault
7 Kohlhase, Michael
7 Nipkow, Tobias
7 Wiedijk, Freek
6 Carette, Jacques
6 Fleuriot, Jacques D.
6 Hales, Thomas Callister
6 Kunčar, Ondřej
6 Maggesi, Marco
6 Owens, Scott
6 Rashid, Adnan
6 Siddique, Umair
5 Aravantinos, Vincent
5 Böhme, Sascha
5 Krauss, Alexander
5 McLaughlin, Sean
5 Théry, Laurent
5 Traytel, Dmitry
5 Wenzel, Makarius
4 Adams, Mark
4 Akbarpour, Behzad
4 Amjad, Hasan
4 Arthan, Rob D.
4 Bertot, Yves
4 Coghetto, Roland
4 Fontaine, Pascal
4 Geuvers, Jan Herman
4 Li, Ximeng
4 Li, Yongdong
4 Magron, Victor
4 Melquiond, Guillaume
4 Müller, Dennis
4 Obua, Steven
4 Solovyev, Alexey
4 Sutcliffe, Geoff
4 Wang, Guohui
3 Avigad, Jeremy
3 Divasón, Jose
3 Färber, Michael
3 Khan Afshar, Sanaz
3 Korniłowicz, Artur
3 Kühlwein, Daniel
3 Li, Liming
3 Mahmoud, Mohamed Yousri
3 Norrish, Michael
3 Papapanagiotou, Petros
3 Sewell, Peter
3 Voronkov, Andrei
3 Weber, Tjark
3 Werner, Benjamin
3 Zhang, Jingzhi
2 Allamigeon, Xavier
2 Aspinall, David
2 Barrett, Clark W.
2 Boldo, Sylvie
2 Boulton, Richard J.
2 Brown, Chad Edward
2 Chen, Shanyan
2 Davis, Jared
2 de Moura, Leonardo
2 De Oliveira, Diego Caminha B.
2 Déharbe, David
2 Dekdouk, Abdelkader
2 Gopalakrishnan, Ganesh Lalitha
2 Grabowski, Adam
2 Grégoire, Benjamin
2 Hurd, Joe
2 Janičić, Predrag
2 Keller, Chantal
2 Lelay, Catherine
2 Lewis, Robert Y.
2 Ma, Sha
2 Mahboubi, Assia
2 Moskal, Michał
2 Narboux, Julien
2 Naumowicz, Adam
2 Pąk, Karol
2 Pichardie, David
2 Rahli, Vincent
2 Roux, Cody
2 Rümmer, Philipp
2 Scott, Phil
2 Seddiki, Ons
2 Sibut-Pinote, Thomas
2 Sojka, Petr
2 Steen, Alexander
...and 289 more Authors
all top 5

Cited in 40 Serials

44 Journal of Automated Reasoning
14 Lecture Notes in Computer Science
11 Journal of Formalized Reasoning
8 Formal Aspects of Computing
5 MSCS. Mathematical Structures in Computer Science
4 Journal of Symbolic Computation
4 Formal Methods in System Design
4 Journal of Applied Logic
4 Mathematics in Computer Science
4 Formalized Mathematics
3 ACM Transactions on Mathematical Software
3 Advances in Applied Clifford Algebras
3 Journal of Functional Programming
3 Logical Methods in Computer Science
3 Journal of Logical and Algebraic Methods in Programming
2 Theoretical Computer Science
2 Information and Computation
2 Annals of Mathematics and Artificial Intelligence
2 Electronic Notes in Theoretical Computer Science
1 American Mathematical Monthly
1 Artificial Intelligence
1 Jahresbericht der Deutschen Mathematiker-Vereinigung (DMV)
1 The Mathematical Intelligencer
1 Journal of Computer and System Sciences
1 Science of Computer Programming
1 Annals of Pure and Applied Logic
1 Discrete & Computational Geometry
1 Notices of the American Mathematical Society
1 Experimental Mathematics
1 Bulletin of the Belgian Mathematical Society - Simon Stevin
1 The Bulletin of Symbolic Logic
1 Fundamenta Informaticae
1 Journal of Applied Mathematics
1 Sādhanā
1 Computer Languages, Systems & Structures
1 Journal of Software
1 Logica Universalis
1 Forum of Mathematics, Pi
1 Proceedings of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences
1 Journal of Applied Logics - IfCoLog Journal of Logics and their Applications

Citations by Year