HOL（高階邏輯）表示一個使用類似（高階）邏輯和實現策略的交互式定理證明系統家族。這個系列的系統遵循LCF的方法，因為它們被實現為一個庫，該庫定義了一個被證明的定理的抽象數據類型，這樣，這種類型的新對象只能使用庫中對應于高階邏輯推理規則的函數來創建。只要這些函數被正確實現，系統中所有被證明的定理都必須是有效的。因此，一個大的系統可以建立在一個小的可信內核之上。HOL家族中的系統使用ML或其繼承者。ML最初是和LCF一起開發的，作為定理證明系統的元語言；事實上，這個名字代表了元語言。

HOL系統使用經典高階邏輯的變體，它有簡單的公理基礎，公理很少，語義很好理解。HOL證明器中使用的邏輯與Isabelle/HOL密切相關，后者是Isabelle中使用最廣泛的邏輯。HOL的實現盡管HOL是Isabelle的前身，但各種HOL的衍生物仍在活躍使用。這就是目前的四個HOL系統（共享本質上相同的邏輯）。HOL4--目前xxx被維護和開發的系統，源于HOL88系統，它是由MikeGordon領導的原始HOL實現工作的高潮。HOL88包括它自己的ML實現，它又是在CommonLisp的基礎上實現的。HOL88之后的系統（HOL90、HOL98和HOL4）都是用標準ML實現的；而HOL98是與MoscowML耦合的，HOL4可以用MoscowML或Poly/ML構建。所有這些都帶有大量的定理證明代碼庫，在非常簡單的核心代碼之上實現額外的自動化。

HOL4是BSD授權的。HOLLight-HOL的一個實驗性極簡版本，后來發展成為另一個主流的HOL變體；其邏輯基礎仍然異常簡單。HOLLight最初用CamlLight實現，現在使用OCaml。HOLLight在新的BSD許可下可用。ProofPower-一組工具，旨在為使用形式化規范的Z符號工作提供特殊支持。6個工具中有5個是GNUGPLv2許可的。第六個(PPDaz)有一個專有許可證。HOLZero-一個專注于可信度的最小化實現。HOLZero是GNUGPL3+許可的。形式證明的發展CakeML項目為ML開發了一個形式證明的編譯器。