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.
More on
the history of HOL and related systems.
TPHOLS Conference
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
logics.
Mailing lists for HOL
Links
|
