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 137 articles )
Showing results 1 to 20 of 137.
Sorted by year (- 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)
- 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)
- Rabe, Florian: The future of logic: foundation-independence (2016)
- Siddique, Umair; Tahar, Sofiène: On the formal analysis of Gaussian optical systems in HOL (2016)
- Benzmüller, Christoph; Sultana, Nik; Paulson, Lawrence C.; Theiß, Frank: The higher-order prover Leo-II (2015)
- Boldo, Sylvie; Lelay, Catherine; Melquiond, Guillaume: Coquelicot: A user-friendly library of real analysis for Coq (2015)
- Davis, Jared; Myreen, Magnus O.: The reflective Milawa theorem prover is sound (down to the machine code that runs it) (2015)
- de Moura, Leonardo; Kong, Soonho; Avigad, Jeremy; van Doorn, Floris; von Raumer, Jakob: The Lean theorem prover (system description) (2015)
- Fukasaku, Ryoya; Inoue, Shutaro; Sato, Yosuke: On QE algorithms over an algebraically closed field based on comprehensive Gröbner systems (2015)
- Hales, Thomas C.: Developments in formal proofs (2015)
- Harrison, John: Formal proofs of hypergeometric sums. Dedicated to the memory of Andrzej Trybulec (2015)
- Jacobsen, Charles; Solovyev, Alexey; Gopalakrishnan, Ganesh: A parameterized floating-point formalizaton in HOL Light (2015)
- Kaliszyk, Cezary: Efficient low-level connection tableaux (2015)
- Kaliszyk, Cezary; Urban, Josef: MizAR 40 for Mizar 40 (2015)
- Kaliszyk, Cezary; Urban, Josef: HOL(y)Hammer: online ATP service for HOL Light (2015)
- Kaliszyk, Cezary; Urban, Josef: Learning-assisted theorem proving with millions of lemmas (2015)