Higher-Order Logic
Higher-Order Logic
m Investigated extensively by Gordon [M. Gordon 85-88].
m HOL mechanized for verification by R. Milner on LCF. LCF implemented in ML (the LCF Meta-language).
m Proof in HOL is achieved by repeatedly applying inference rules to axioms or to previously proved theorems.