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.
Platform: Linux, MacOS, Windows with Cygwin or WSL
Poly/ML version: >5.7.1
Project link: https://hol-theorem-prover.org