Filter
Top Products
Acknowledgements
HOL Light is one of a long line of ‘HOL’ theorem provers that have been released
into the public domain for applications in academia, industry and government or-
ganizations.
Most of the important ideas behind the software, and many of the same func-
tions and keywords, are taken from the original version of HOL, written by Mike
Gordon. This in turn drew directly from the Edinburgh LCF project led by Robin
Milner (and including Lockwood Morris, Malcolm Newey, Mike Gordon and Chris
Wadsworth in the team), and some of the reengineering and rationalization of the
system by Larry Paulson. Early versions of HOL were honed into successful tools
by many people in the University of Cambridge and further afield, especially Tom
Melham.
HOL Light began as a distillation of the simple core parts of HOL, which was
done in collaboration with Konrad Slind, based on his hol90 system. The rest of
the system was written gradually over the course of several years by John Harrison,
and eventually practically all of the original hol90 code was rewritten. Although
this is the first public release, several people have used the system, made helpful
suggestions and pointed out bugs. Thanks to Donald Syme, B Karthikeyan, Michael
Norrish and Mark Woodcock, among others.
v