HOL4 is a proof assistant for higher-order logic.

See Also