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 all top 5 Referenced in 37 Serials 41 Journal of Automated Reasoning 14 Lecture Notes in Computer Science 11 Journal of Formalized Reasoning 7 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 Logical Methods in Computer Science 2 Theoretical Computer Science 2 Information and Computation 2 Journal of Functional Programming 2 Annals of Mathematics and Artificial Intelligence 2 Electronic Notes in Theoretical Computer Science 2 Journal of Logical and Algebraic Methods in Programming 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 Discrete & Computational Geometry 1 Notices of the American Mathematical Society 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 all top 5 Referenced in 30 Fields 286 Computer science (68-XX) 72 Mathematical logic and foundations (03-XX) 17 General and overarching topics; collections (00-XX) 17 Numerical analysis (65-XX) 12 Number theory (11-XX) 7 Real functions (26-XX) 6 Geometry (51-XX) 5 Linear and multilinear algebra; matrix theory (15-XX) 5 Convex and discrete geometry (52-XX) 5 Optics, electromagnetic theory (78-XX) 5 Operations research, mathematical programming (90-XX) 4 History and biography (01-XX) 3 Functions of a complex variable (30-XX) 3 Special functions (33-XX) 3 Harmonic analysis on Euclidean spaces (42-XX) 3 Quantum theory (81-XX) 2 Commutative algebra (13-XX) 2 General topology (54-XX) 2 Systems theory; control (93-XX) 1 Combinatorics (05-XX) 1 Algebraic geometry (14-XX) 1 Several complex variables and analytic spaces (32-XX) 1 Ordinary differential equations (34-XX) 1 Integral transforms, operational calculus (44-XX) 1 Functional analysis (46-XX) 1 Calculus of variations and optimal control; optimization (49-XX) 1 Algebraic topology (55-XX) 1 Manifolds and cell complexes (57-XX) 1 Mechanics of particles and systems (70-XX) 1 Mathematics education (97-XX) Referencing Publications by Year