HOL is typed, but not a dependent type theory. HOL is also a classical logic. HOL is essentially Alonzo Church's simply typed lambda-calculus [1] from 1940. Cla

HOL is typed, but not a dependent type theory. HOL is also a classical logic. HOL is essentially Alonzo Church's simply typed lambda-calculus [1] from 1940. Classical, rather than constructive logic tends to give shorter proofs. [1] A. Church, A Formulation of the Simple Theory of Types. https://pdfs.semanticscholar.org/28bf/123690205ae5bbd9f8c84b1330025e8476e4.pdf https://pdfs.semanticscholar.org/28bf/123690205ae5bbd9f8c84b...