The HOL System
The HOL System is an environment for interactive theorem proving in a
higher-order logic. Its most outstanding feature is its high degree of
programmability through the meta-language ML. The system has a wide
variety of uses from formalizing pure mathematics to verification of
industrial hardware. Academic and industrial sites world-wide are using HOL.
The name `HOL' is pronounced either as a word to rhyme with `doll' or letter
by letter. The system is available without charge.
Download the latest public release of the HOL System.
the history of HOL and related systems.
There has been a series of international conferences on
the HOL System. The first three were informal users'
meetings with no published proceedings. The tradition now is for an annual
conference in a continent different to the location of the previous meeting.
From 1996 the scope broadened to cover all theorem proving in higher-order
Mailing lists for HOL