HOL Light

HOL Light is an interactive LCF-style theorem prover for classical higher order logic. It is a clean redesign by John Harrison of the original HOL system designed by Mike Gordon in the 1980s. It is intended to help in the construction of formal proofs in pure mathematics or system verification.

More information

• HOL Light home page: http://www.cl.cam.ac.uk/~jrh13/hol-light/
• Tutorial: http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial.pdf
• Reference manual PDF: http://www.cl.cam.ac.uk/~jrh13/hol-light/reference.pdf

Related Google Code projects

• HOL Online: http://code.google.com/p/hol-online/
• Flyspeck: http://code.google.com/p/flyspeck/