HOL Light
Table of Contents
I've been thinking about implementing a HOL kernel in Standard ML, just
for fun. HOL Light has an implementation in a tiny kernel about 396
lines long (excluding 128 blank lines and 148 comment lines, as of git
commit 970121c on Sep 12, 2016).
1. Get Started
I'm assuming you've downloaded and compiled HOL Light successfully. Start up OCaml, then:
# #use "hol.ml";;
This will load HOL Light into the OCaml repl. If you additionally want
to use miz3 mode, you can then run:
# #use "miz3/miz3.ml";;
There are also some emacs macros written for HOL Light.
2. Obtaining and Compiling
- Compiling HOL Light has some gotchas
3. Some Examples
- Library/grouptheory.ml is where some group theory is done
4. References
- HOL Light Reference (PDF, HTML)
- John Harrison, Tutorial for version 220 (although dated, still useful).
- Felix Breuer, Formal proof - first steps with HOL Light; blog post dated June 11, 2012.
4.1. Neat Applications of HOL Light
- O. Kunčar,
"Reconstruction of the Mizar Type System in the HOL Light System".
PDF, 6 pages. - Petros Papapanagiotou and Jacques Fleuriot,
"Object-Level Reasoning with Logics Encoded in HOL Light".
arXiv:2101.03808, 17 pages - Lawrence C. Paulson,
"Formalising Mathematics in Simple Type Theory".
arXiv:1804.07860, 17 pages. - Adnan Rashid and Osman Hasan,
"Formalization of Lerch's Theorem using HOL Light".
arXiv:1806.03049, 30 pages. - Chantal Keller, Benjamin Werner,
"Importing HOL Light into Coq".
inria-00520604, 17 pages.
4.2. Papers about implementation details
- Freek Wiedijk,
"Stateless HOL".
arXiv:1103.3322, 15 pages. - Ramana Kumar,
"Self-compilation and self-verification".
PhD Thesis, Cambridge 2017, PDF
4.3. Other related references
- Ben Lynn, Let there be HOL Light for a code golf implementation of HOL Light
- Magnus O. Myreen, Scott Owens, and Ramana Kumar,
"Steps Towards Verified Implementations of HOL Light".
PDF, 6 pages, published in Proc. ITP 2013, pp.490–495.
4.4. HOL in general
- William M. Farmer,
"The Seven Virtues of Simple Type Theory".
doi:10.1016/j.jal.2007.11.001, 2008 - The HOL System Description (LaTeX files), for HOL4