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

Links

  Long-term projects
HOL
Isabelle




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