The Laboratory for Applied Logic at Brigham Young University is pleased to provide documentation and information about the HOL Theorem Proving System . Standard HOL Documentation Description Manual Tutorial Manual Library Manual Case Studies Learning to Use HOL New users are encouraged to join the info-hol mailing list.
New users are welcome to ask questions.
Phil Windley has written a tutorial on using HOL , and there is a version for HOL90 . The first part of the tutorial is general and the last part discusses hardware verification. Mike Gordon has a two part course in Specification and Verification available on-line. An overview paper is available . Kathi Fisler has put together a tutorial for HOL90 beginners Tom Melham has made his training materials available on the HOL system and its applications .