Introduction to HOL A theorem proving environment for higher order logic Edited by M. J. C. Gordon and T. F. Melham Cambridge University Press, 1993. 228 x 152 mm; 496 pages. ISBN 0-521-44189-7.

The book is an edited version of a combination of the HOL tutorial and system description, published in a format suitable for convenient reference at the terminal as well as reading. The purpose of this volume was to provide a coherent and self-contained introduction to HOL and to extract and compress from various sources most of the material needed for day-to-day work with the system.

After a quick overview that gives a hands-on feel for the way HOL is used, there follows a detailed description of the HOL meta-language ML. Part III then presents the logic that HOL supports. Part IV describes how HOL is embedded in ML, and Part V then explains the theorem-proving infrastructure provided by HOL. Finally, two appendices contain a subset of the reference manual and a survey of the HOL libraries, including an example of the documentation for an actual HOL library.

All royalties from this book go into a fund to support the HOL system and HOL-based activities.

You and read a review by Graham Hutton in the Journal of Functional Programming, 4(4):557-559, 1994.