HOL
Table of Contents
1. Introduction
Broadly, HOL refers to a family of theorem provers which emerged out of LCF, using similar techniques applied to higher-order logic as Church presented it in his article on simple-type theory.
It turns out HOL is a metalogical framework. One way to encode inductive datatypes, for example, may be found in John Harrison's tutorial on HOL Light in section 15.
2. References
- Mike Gordon,
"HOL: A Machine Oriented Formulation of Higher Order Logic".
Tech Report 68, Cambridge University, July 1985. - Thomas F. Melham,
"Automating Recursive Type Definitions in Higher Order Logic".
In Current Trends in Hardware Verification and Automated Theorem Proving, edited by G. Birtwistle and P. A. Subrahmanyam (Springer-Verlag, 1989), pp. 341–386. PDF - M. J. C. Gordon and T. F. Melham,
Introduction to HOL: A theorem proving environment for higher order logic.
Cambridge University Press, 1993. - Anthony Bordg, Lawrence Paulson, Wenda Li,
"Simple Type Theory is not too Simple: Grothendieck's Schemes without Dependent Types".
arXiv:2104.09366, 31 pages
2.1. Simple Type Theory
- Lawrence Paulson,
"A Formulation of the Simple Theory of Types (for Isabelle)".
Tech. Rept. UCAM-CL-TR-175, dated 2 August 1989, eprint; 32 pages. - Church’s Type Theory, entry in Stanford Encyclopedia of Philosophy
- Alanzo Church,
"A Formulation of the Simple Theory of Types".
The Journal of Symbolic Logic 5 no.2 (1940) 56–68. JSTOR. - Peter B. Andrews,
An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof.
Second ed., Springer, 2002.- Probably the best introduction to higher-order logic mathematically.