"Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic" - читать интересную книгу автора (M. J. C. Gordon, T. F. Melham)