Automated Reasoning Group

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


  Long-term projects

Lab Publications
Technical Reports
Last modified on Wed May 9 23:10:47 BST 2012 by ns441 | Privacy policy