HOL theorem-proving system / News: Recent posts

Kananaskis-5 released

We are pleased to announce the release of the latest version of the HOL4 system. Among the many, many, exciting new features are support for another SML implementation (Poly/ML) and new parsing/printing facilities, including extensive support for Unicode characters. Replace ``!x. P x`` with ``∀x. P x`` today!

Posted by Michael Norrish 2009-07-09

Kananaskis-4 released

Our latest version of HOL4, Kananaskis-4 has been released. It includes a number of powerful new features, as well as improved documentation and bug-fixes.

Posted by Michael Norrish 2007-01-03

Kananaskis-3 released

The latest version of HOL4, Kananaskis-3 has been released. For more information on its new features and bug-fixes, see http://hol.sourceforge.net/kananaskis-3.release.html

Posted by Michael Norrish 2006-01-02

Timing bug in Moscow ML!

Kananaskis-1 has been made pretty well unusable because of a time overflow problem in the underlying Moscow ML v2.00. The working version in CVS has been fixed (for downloading from CVS see http://sourceforge.net/cvs/?group_id=31790 for instructions), at least for non-Windows users.

You can also download a new version of Moscow ML from its home-page at
http://www.dina.dk/~sestoft/mosml.html. You will
need to rebuild Moscow ML, and then all of HOL. There will hopefully be a Windows version of 2.01 available soon.... read more

Posted by Michael Norrish 2004-01-13

Kananaskis-1 release of HOL theorem-proving system

Our first fully S/F-ed release of HOL is now
available. See the home-page at

Posted by Michael Norrish 2002-06-21