HOL

Higher Order Logic

A proof-generating system for higher order logic based on LCF.

"HOL: A Machine Oriented Formulation of Higher Order Logic", M. J. C. Gordon, Report 68, Computer Lab Cambridge University (1985).

Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, M. J. C. Gordon et al eds, Cambridge University Press, 1993. ISBN 0-521-441897

HOL-88

Built on ML[2], from Mike Gordon

HOL-90

Built on SML/NJ, from Brian Graham