There are three other systems implementing the same logic as HOL4: HOL Light, by John Harrison and written in OCaml; ProofPower, by Rob Arthan and written in SML; and HOL Zero, by Mark Adams and written in OCaml.

The HOL provided by the Isabelle system (often written “Isabelle/HOL”) is very similar to the higher order logic of HOL4, HOL Light and ProofPower, but has a type system with Haskell-like type-classes.

The PVS system has a type system with predicate sub-typing. Getting a term (formula, definition) to typecheck can require arbitrary amounts of work, but definitions are a deal more expressive.

The HOL-ω
system implements a
sophisticated type system (like that of *System F _{ω}*)
that also remains a superset of HOL4’s. In terms of implementation,
the system is also a drop-in replacement for HOL4: all existing HOL4
scripts should continue to work as before in HOL-ω.

- Hogwarts Online (top Google hit)
- The IKEA HOL side table
- Hellas Online
- Human Occupied Landfill