×

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; Flyspeck; PVS; z3; ACL2; E Theorem Prover; TPTP; VAMPIRE; Agda; Sledgehammer; kepler98; Nuprl; Metis_; Archive Formal Proofs; Isar
Referenced in: 301 Publications
all top 5

Referenced by 361 Authors

35 Kaliszyk, Cezary
23 Urban, Josef
16 Tahar, Sofiène
15 Rabe, Florian
12 Blanchette, Jasmin Christian
10 Hasan, Osman
10 Popescu, Andrei
9 Paulson, Lawrence Charles
8 Guan, Yong
8 Kumar, Ramana
8 Myreen, Magnus O.
7 Farmer, William M.
7 Gauthier, Thibault
7 Kohlhase, Michael
7 Nipkow, Tobias
7 Shi, Zhiping
7 Wiedijk, Freek
6 Benzmüller, Christoph Ewald
6 Carette, Jacques
6 Hales, Thomas Callister
6 Kunčar, Ondřej
6 Owens, Scott
6 Siddique, Umair
5 Aravantinos, Vincent
5 Böhme, Sascha
5 Fleuriot, Jacques D.
5 Krauss, Alexander
5 McLaughlin, Sean
5 Théry, Laurent
5 Traytel, Dmitry
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, Yongdong
4 Maggesi, Marco
4 Magron, Victor
4 Melquiond, Guillaume
4 Müller, Dennis
4 Obua, Steven
4 Rashid, Adnan
4 Solovyev, Alexey
4 Wenzel, Makarius
3 Avigad, Jeremy
3 Färber, Michael
3 Khan Afshar, Sanaz
3 Korniłowicz, Artur
3 Kühlwein, Daniel
3 Li, Liming
3 Li, Ximeng
3 Mahmoud, Mohamed Yousri
3 Norrish, Michael
3 Sewell, Peter
3 Sutcliffe, Geoff
3 Voronkov, Andrei
3 Wang, Guohui
3 Weber, Tjark
3 Werner, Benjamin
2 Allamigeon, Xavier
2 Aspinall, David
2 Barrett, Clark W.
2 Boldo, Sylvie
2 Boulton, Richard J.
2 Brown, Chad Edward
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 Papapanagiotou, Petros
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 Tankink, Carst
2 Völker, Norbert
2 Wintersteiger, Christoph M.
2 Wolff, Burkhart
2 Yamada, Akihisa
...and 261 more Authors

Referencing Publications by Year