Owner: michaeln
Category: Application
Proof assistant for higher order logic
Ultimately deriving from Gordon's HOL88, HOL4 is the latest version of this interactive theorem-proving system. It supports a tactic-based approach to proof, using the LCF approach that led to ML's invention as a programming language.
Dependencies: None
Platform: Linux, MacOS, Windows with Cygwin or WSL
Poly/ML version: >5.7.1
Licence: BSD
Download link: https://github.com/HOL-Theorem-Prover/HOL/archive/kananaskis-13.tar.gz
Project link: https://hol-theorem-prover.org