Automated Reasoning Group HOL page
Lab |
ARG |
Description |
HOL |
Isabelle |
Members |
Haiku
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.
Click for
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.
The next TPHOLS conference will be held in
Kaiserslautern,
Germany.
More on
conferences.
Email for HOL
Links
Lab |
ARG |
Description |
HOL |
Isabelle |
Members |
Haiku
Page last updated on Thu Sep 21 15:43:04 BST 2006
by Juliano Iyoda
(jmi27@cl.cam.ac.uk)