Intuition for HOL

Untyped Lambda Calculus

Simply Typed Lambda Calculus

Further reading:

• Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam (1984)
• H. P. Barendregt: Lambda Calculi with Types

Syntax and Shorthands of HOL

Standard-Model Semantics of HOL

Axioms of HOL

Results Proved in HOL

Further reading:

• Peter B. Andrews: An Introduction to Mathematical Logic and Type theory: To Truth through Proof, Springer 2002 (Chapter 5: Type Theory)
• The Seven Virtues of Simple Type Theory

Approaches to Reliable Complex Proofs

Immutable Abstract Data Types

Theorems as Abstract Data Types

Proof and Code Generation in LCF Systems

Binary Search Trees Example

Further reading:

• A Metalanguage for interactive proof in LCF - ML stands for meta-Language, because it was a language for writing theorem provers that prove theorems (in object-language i.e. logic of computable functions)
• HOL Light
• Handbook of Practical Logic and Automated Reasoning by John Harrison

HOL - use directly ML

HOL Light - compact version, written in OCaml

Isabelle - popular, ML part largely hidden

PVS - automation through decision procedures

Coq - also very popular, more automation introduced recently; more complex logic

NuPRL - more complex type theory, constructive mathematics

ACL2 - emphasis on executable functions, quantifier-free statements, automated induction, pioneering industrial-scale case studies