HOL

Higher Order Logic. A proof-generating system for higherorder logic based on LCF. Implementations include HOL-88

and HOL-90.

. Mailing list:

[email protected].

["HOL: A Machine Oriented Formulation of Higher Order Logic",

M.J.C. Gordon, Report 68, Comp Lab U Cambridge (1985)].

["Introduction to HOL", M.J.C. Gordon et al, Cambridge U Press

1993 ISBN 0-521-441897].