The HOL interactive theorem prover is a proof assistant for higher-order logic: a programming environment in which theorems can be proved and proof tools implemented. Built-in decision procedures and theorem provers can automatically establish many simple theorems (users may have to prove the hard theorems themselves!) An oracle mechanism gives access to external programs such as SMT and BDD engines. HOL is particularly suitable as a platform for implementing combinations of deduction, execution and propert
Other HOLs are described elsewhere.
HOL is free software, released under the Modified (3-clause) BSD licence .
CakeML
Poly/ML Home Page
AIPLANS Workshop | Advances in Programming Languages and Neurosymbolic Systems workshop at NeurIPS 2021
Interactive Theorem Proving
Proof Engineering
Machine Logic
Karl Palmskog
Yong Kiam Tan
Thomas Türk
Logictools
Thibault Gauthier
Thomas Türk
Formal Methods & Industry