HOL (proof assistant)

GCL是一些大型项目所选择的实现，包括数学工具Maxima、AXIOM（英语：Axiom (computer algebra system)）、HOL88（英语：HOL (proof assistant)）和ACL2。GCL运行在Linux上的十一种架构下，还有FreeBSD、Solaris、Mac OS X和Microsoft

所有这些实现都是开源的并可自由的获得。其中多数用SML实现了自身。不再有任何商业SML实现。 证明辅助器HOL4（英语：HOL (proof assistant)）、Isabelle、LEGO（英语：LEGO (proof assistant)）和Twelf（英语：Twelf）是用Standard ML写成。它还用于编译器制作和集成电路设计比如ARM。

1997. Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel: Isabelle/HOL – A Proof Assistant for Higher-Order Logic. Isabelle 的官方网站 （页面存档备份，存于互联网档案馆） 形式化证明存档（The

LCF，而剑桥大学的Michael J. C. Gordon（英语：Michael J. C. Gordon）用它开发了第一版的HOL（英语：HOL (proof assistant)）。这个ML系统由INRIA和剑桥大学联合维护和发行。 基于Thierry Coquand（英语：Thierry

Nipkow, Tobias; Paulson, Lawrence C.; Wenzel, Markus, Isabelle/Hol: A Proof Assistant for Higher-Order Logic, Springer, 2002, ISBN 3-540-43376-7  Nuerk